Agda (programming language): Difference between revisions

Revision as of 04:08, 17 December 2006

Revision as of 10:28, 10 May 2007

Line 1:

{{context}}

'''Agda''' is an [[Interactive theorem proving|interactive system]] for developing [[constructive proof]]s in a variant of [[Per Martin-Löf]]'s [[Intuitionistic Type Theory|Type Theory]]. It can also be seen as a [[functional programming language]] with [[dependent type]]s.

in a variant of [[Intuitionistic Type Theory|Martin-Löf's Type Theory]]

*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 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==

*[[Intuitionistic Type Theory]]

*[[Per Martin-Löf]]

==External links==

* [http://agda.sf.net/ Agda project home page]

==References==

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

* A. Abel, et al. Verifying [[Haskell (programming language)|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

* A. Abel, et al. Verifying [[Haskell (programming)|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.