Agda (programming language): Difference between revisions

Revision as of 02:57, 11 May 2007

Revision as of 17:03, 18 June 2007

Line 1:

{{context}}

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

'''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 and was developed at [[Chalmers University of Technology]].