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
proofs. 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:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaMeetings
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
sprint.