Agda (theorem prover)
From Seo Wiki - Search Engine Optimization and Programming Languages
|Usual file extensions||.agda, .lagda|
|Stable release||2.2.4 (July 7, 2009)|
|Influenced by||Epigram, Haskell|
Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it 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 by Ulf Norell, a post-doc 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.
The current version of Agda, Agda 2, has been developed at Chalmers by Ulf Norell. The syntax has changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance implicit variables, that can be omitted when deducible from the context. Agda 2 also makes extensive use of Unicode as a way to obtain easily-readable proofs.
Agda 2 provides either a commandline tool or a powerful Emacs mode, developed by Makoto Takeyama and Nils Anders Danielsson.
Agda 2 is similar to Epigram.
- 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.