Agda theorem prover

From Wikipedia, the free encyclopedia

Agda is an interactive system for developing constructive proofs in a variant of Martin-Löf's Type Theory

Agda can also be seen as a functional language with dependent types.

• It 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.

• Has an emacs-interface and a graphical interface, Alfa

[edit] See also

• Intuitionistic Type Theory
• Per Martin-Löf

[edit] External links

• Agda project home page

[edit] 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.