This article provides insufficient context for those unfamiliar with the subject. |
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.
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.
External links
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 mathematics-related article is a stub. You can help Wikipedia by expanding it. |
 | This software article is a stub. You can help Wikipedia by expanding it. |