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.
Agda is open-source and enjoys contributions from many authors. The center of the Agda development is the Programming Logic group at Chalmers and Gothenburg University; the main developers are Ulf Norell, Nils Anders Danielsson, and Andreas Abel.
Agda meetings
Agda users and implementors meet biannually for a week of talks and code sprints.
- The next Agda meeting, AIM XXVII, will be held in Göteborg from 4 to 9 June 2018.
- Past Agda Meetings.
News
- (2018-06-08) The standard library 0.16 is now available.
- (2018-06-02) Agda 2.5.4 is now available.
- (2018-03-12) The standard library 0.15 is now available.
- (2017-09-08) Agda 2.5.3 is now available.
Getting started
- Language tutorials.
- Installation and use.
- 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 (all Agda users are strongly encouraged to add their own developments to make them available to the community).
Further information
Old/outdated stuff
- Feature requests, and discussions about them