Agda (programming language)
|Stable release||184.108.40.206 (October 30, 2013)|
|Influenced by||Coq, Epigram, Haskell|
|License||See the LICENSE file|
Agda is both a functional programming language with dependent types, based on the idea of the Curry-Howard correspondence as embodied in Per Martin-Löf's intuitionistic type theory, and a proof assistant for developing constructive proofs. The latest version of Agda, Agda 2, is a complete rewrite originally developed by Ulf Norell, a research engineer at Chalmers University of Technology.
Agda, unlike Coq, has limited support for tactics and proofs are generally written in functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has an Emacs interface but can also be run in batch mode from the command line.
The current version of Agda is Agda 2. The main difference since Agda 1 is support for a richer family of datatypes and pattern matching on them. Agda 2 also makes extensive use of Unicode as a way to obtain easily readable proofs.
Agda 2 provides a powerful Emacs mode, developed by Makoto Takeyama and Nils Anders Danielsson.
Agda 2 is closely related to Epigram.
- 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
- 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 Takeyama (2006)