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 languagewith 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
Emacsinterface and a graphical interface, Alfa.
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
Unicodeas a way to obtain easily-readable proofs.
Agda 2 provides either a commandline tool or a powerful
Emacsmode, developed by Makoto Takeyama and Nils Anders Danielsson.
The 7th Agda Implementor's Meeting was held in
Osakain 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 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf
* M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. http://www.cs.chalmers.se/~marcin/Papers/universes.pdf
* T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.
* [http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php The Agda 2 homepage] (a wiki), including some documentation and a link to a bugreport tool
* [http://unit.aist.go.jp/cvs/Agda/ 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 … Википедия