Agda (programming language): Difference between revisions

Revision as of 15:54, 29 May 2008

Revision as of 09:33, 15 June 2008

Line 1:

[[Image:Agda_proofAgda proof.jpg|thumb|300px|right|Excerpt of a proof in '''agda2''']]

'''Agda''' is a theorem prover, i.e. a computer program that can check mathematical proofs. More specifically, it 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 and was developed at [[Chalmers University of Technology]].

Line 6:

==Agda 2==

The second version of Agda, Agda 2, is currently being developed at [[Chalmers University of Technology|Chalmers]] by Ulf Norell. The syntax has completely changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance implicit variables, that can be omitted when deduceablededucible from the context. Agda 2 also makes an intensive 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.

Line 23:

* [http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php The Agda 2 homepage] (a wiki), including some documentation and a link to a bugreport tool

* [http://unit.aist.go.jp/cvs/Agda/ Agda version 1 home page]

{{simulation-software-stub}}

[[Category:Functional languages]]

[[Category:Interactive theorem proving software]]

[[Category:Haskell software]]

{{simulation-software-stub}}