Agda (programming language): Difference between revisions

Revision as of 23:44, 17 March 2006

Revision as of 23:52, 17 March 2006

Line 1:

[http://agda.sf.net/ Agda] is an interactive system for developing [[constructive proof]]s

in a variant of [[Per Martin-Löf|Martin Löf]]'s [[type theory]].

Agda can also be seen as a [[functional language]] with [[dependent type]]s.

* 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

==See also==

Line 14 ⟶ 20:

* C. Coquand et al. An emacs-interface for type directed support constructing proofs and programs. ENTCS 2006.

* A. Abel, et al. Verifying {[[Haskell} (programming)|Haskell]] Programs Using Constructive [[Type Theory]], ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005

* 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