Agda

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.

News

• AIM XI will take place Wednesday 24 - Tuesday 30 March, 2010 in Awaji Island, Japan. Call For Participation

Getting started

• Download.
• Language tutorials.
• Quick guide to editing, type checking and compiling Agda code.
• Community: mailing list and IRC channel. Don’t hesitate to ask questions!

Documentation and examples

• Manuals and howtos.
• Standard library, and other libraries and developments (please include your own contributions).
• Martin-Löf type theory, an implementation in Agda.
• Introductory examples from the Agda distribution. Further examples.
• Agsy, an integrated tool for automated proof/term generation.

Further information

• Publications
• Agda Meetings
• Feature requests, and discussions about them
• History