Agda (programming language)
| Paradigm | Functional |
|---|---|
| Stable release | 2.3.0
/ November 23, 2011 |
| OS | Cross-platform |
| License | See the LICENSE file |
| Filename extensions | .agda, .lagda |
| Website | Agda wiki |
| Influenced by | |
| Coq, Epigram, Haskell | |
Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs based on the Curry-Howard correspondence in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types. Agda was developed by Ulf Norell, a postdoctoral researcher 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.
As a programming language, Agda has Haskell-like syntax, and the Agda 2 compiler can convert Agda proofs into functions in the Haskell, JavaScript, or Epic languages.
Agda 2
The current version of Agda, Agda 2, has been developed at Chalmers by Ulf Norell. The syntax has 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 extensive 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 10th Agda Implementor's Meeting was held in Gothenburg in September 2009. AIM11 is scheduled for March in Japan.
Agda 2 is similar to Epigram.
References
- C. Coquand et al. An Emacs interface for type directed support constructing proofs and programs. ENTCS 2006. https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf
- 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://www.cse.chalmers.se/~ulfn/papers/fol.pdf
External links
- The Agda 2 homepage (a wiki), including documentation and a link to a bug-report tool
- Agda at the Hackage repository
- Learn you an Agda, a tutorial.
- A course on Functional Programming, with seven parts on Agda
- Introduction to Agda, a five-part YouTube playlist by Daniel Peebles
- Dependently Typed Programming in Agda, by Ulf Norell
- A Brief Overview of Agda, by Ana Bove, Peter Dybjer, and Ulf Norell
- An Agda Tutorial, Misao Nagayama, Hideaki Nishihara, Makoto Takeyam (2006)
 | This logic-related article is a stub. You can help Wikipedia by expanding it. |
 | This programming-language-related article is a stub. You can help Wikipedia by expanding it. |