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
- Agda Implementors’ Meeting XVII will be held 8–14 May 2013 in Japan.
- (2012/11/12) Agda 2.3.2 has been released! Get it here: Download.
- (2012/03/12) Agda 2.3.0.1 is out. It is the same as Agda 2.3.0 but compatible with ghc-7.4.1. Download.
- (2011/11/23) Agda 2.3.0 is out! Get it while it’s hot: Download.
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 (all Agda users are strongly encouraged to add their own developments to make them available to the community).
Further information
- Publications
- Agda Meetings
- Feature requests, and discussions about them
- History