Agda (programming language): Difference between revisions

Revision as of 01:58, 11 September 2009

Revision as of 15:48, 17 September 2009

Line 26:

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

The secondcurrent version of Agda, Agda 2, is currentlyhas beingbeen 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 deducible from the context. Agda 2 also makes extensive 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.

The 7th10th Agda Implementor's Meeting was held in [[OsakaGothenburg]] in NovemberSeptember 20072009. AIM8AIM 11 is scheduled for MayMarch in [[GothenburgJapan]].

Agda 2 is very closesimilar to [[Epigram (programming language)|Epigram]].

==References==