Agda (programming language)

Agda is an interactive system for developing constructive proofs in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types and was developed at Chalmers University of Technology.

Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script. The language has ordinary programming constructs such as data-types and case-expressions, signatures and records, let-expressions and modules. The system has an emacs-interface and a graphical interface, Alfa.

Agda 2

The second version of Agda, Agda 2, is currently being developed at Chalmers by Ulf Norell. The syntax has completely changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance implicit variables, that can be omitted when deduceable from the context. Agda2 also makes an intensive use of Unicode as a way to obtain easily-readable proofs.

The 6th Agda Implementor's Meeting was held in Göteborg in May 2007. AIM7 is scheduled for november in Osaka and should focus on the transition from Agda 1 to Agda 2.

External links

Agda project home page
The Agda wiki, including some documentation and a bugreport tool

References

C. Coquand et al. An emacs-interface for type directed support constructing proofs and programs. ENTCS 2006.
A. Abel, et al. Verifying Haskell Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf
M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. http://www.cs.chalmers.se/~marcin/Papers/universes.pdf
T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.

This software article is a stub. You can help Wikipedia by expanding it.