Content deleted Content added
terminology |
Adding information about the author. |
||
Line 1:
[[Image:Agda proof.jpg|thumb|300px|right|Excerpt of a proof in '''agda2''']]
'''Agda''' is a [[proof assistant]], 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 by [[Ulf Norell]], a post-doc 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.
| |||