Agda (theorem prover)

Agda is a theorem prover, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types 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.

Agda 2

The second version of Agda, Agda 2, is currently being developed at 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 an intensive 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 7th Agda Implementor's Meeting was held in Osaka in November 2007. AIM8 is scheduled for May in Gothenburg.

Agda 2 is very close to Epigram.


* C. Coquand et al. An Emacs interface for type directed support constructing proofs and programs. ENTCS 2006.
* A. Abel, et al. Verifying Haskell Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September, 2005
* M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003.
* T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.

External links

* [ The Agda 2 homepage] (a wiki), including some documentation and a link to a bugreport tool
* [ Agda version 1 home page]

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Agda — may refer to * A minor character from The Hitchhiker s Guide to the Galaxy * The Agda (theorem prover) …   Wikipedia

  • Demostración automática de teoremas — Saltar a navegación, búsqueda Para otros usos de este término, véase Demostración. La demostración automática de teoremas (de siglas ATP, por el término en inglés …   Wikipedia Español

  • Coq — For the coenzyme and dietary supplement, see Coenzyme Q10. Coq Paradigm(s) Functional Stable release 8.3 (October 2010; 12 months ago (2010 10)) …   Wikipedia

  • Haskell — Класс языка: функциональный, ленивый, модульный Тип исполнения: компилируемый, интерпретируемый Появился в: 1990 …   Википедия

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.