Agda (programming language): Difference between revisions

Revision as of 17:55, 12 December 2006

Revision as of 23:01, 12 December 2006

Line 1:

'''Agda''' is an interactive system for developing [[constructive proof]]s

in a variant of [[PerIntuitionistic Type Theory|Martin-Löf|Martin Löf]]'s [[typeType theoryTheory]].

Agda can also be seen as a [[functional language]] with [[dependent type]]s.

Line 12:

==See also==

*[[Intuitionistic Type Theory]]

*[[Per Martin-Löf]]

==External links==