Agda Implementors Meeting

NII Shonan Meeting:

@ Shonan Village Center, Sep. 8-14, 2011

NII Shonan Meeting Report (ISSN 2186-7437): No. 2011-2


  • Peter Dybjer (Chalmers University of Technology)
  • Yoshiki Kinoshita (AIST)
  • Shin-Cheng Mu (Academia Sinica)



Agda is a dependently typed functional programming language. It has
inductive families, i.e., data types which depend on values, such as the type of
vectors of a given length. It also has parametrised modules, mixfix operators,
Unicode characters, and an interactive Emacs interface which can assist the
programmer in writing the program.
Agda is a proof assistant. It is an interactive system for writing and checking
Agda is based on intuitionistic type theory, a foundational system for
constructive mathematics developed by the Swedish logician Per Martin-Löf. It
has many similarities with other proof assistants based on dependent types, such
as Coq, Epigram, Matita and NuPRL.
The Agda Intensive Meetings (called Agda Implementors Meetings in the earlier
days) have been held twice a year in principle since 2004. The record of recent
meetings can be found in the following URL:
The AIM meetings are really “Agda Users and Implementors Meetings,” that is,
meetings where Agda users and implementors get together and exchange ideas,
write Agda code, while simultaneously implementors work on modifications of
the Agda system.
The AIM meeting usually consists of talks and code sprint sessions. Talks are
invited by the organiser, and all participants are expected to propose his/her own
project for a code sprint session.
At the start of AIM, the participants get together and are expected to participate
in projects they wish to take a part in. Then it is discussed which project to
start. A short meeting is held at the end of every day so that each project
reports its progress. A longer meeting is held at the end of the whole AIM to
summarize the result and future of the project.
Everyone who is seriously interested in Agda, not only implementors but those
who are willing to write code in Agda or documentation about Agda is welcome to
the meeting. They are expected to make a constructive contribution to the code



  1. Due to the organization of ICFP, I attended the meeting only for the first day. I enjoyed the morning session, where about 10 interesting topics were proposed and discussed, and several small groups were formed.

  2. Participant

    Very good work atmosphere! Very careful excursion organisation!
    Very relaxed athmosphere!

  3. Participant

    Good meeting, I got lots of work done. Bad:Pillar in the middle of the room. More traditional Japanese location would perhaps be better than the plain modern building we used.