Agda (programming language): Difference between revisions

Revision as of 22:55, 3 July 2008

Revision as of 03:35, 8 November 2008

Line 1:

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

'''Agda''' is a theorem[[proof proverassistant]], 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]].

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.