Agda (programming language)

From Wikipedia, the free encyclopedia
  (Redirected from Agda (theorem prover))
Jump to: navigation, search
Paradigm(s) Functional
Stable release / June 20, 2014 (2014-06-20)
Influenced by Coq, Epigram, Haskell
OS Cross-platform
License See the LICENSE file
Filename extension(s) .agda, .lagda
Website Agda wiki
Excerpt of a proof in agda2

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[1] but can also be run in batch mode from the command line.

There are three compiler backends, MAlonzo which targets Haskell, a JavaScript backend, and an Epic backend.

Agda 2[edit]

The current version of Agda is Agda 2. The main difference from 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.

The 16th Agda Implementor's Meeting was held in Copenhagen in October 2012.[2] The next one is scheduled for spring in Japan.

Agda 2 is closely related to Epigram.


  1. ^ Coquand, Catarina; Synek, Dan. "An Emacs interface for type directed support constructing proofs and programs". European Joint Conferences on Theory and Practice of Software 2005. 
  2. ^ "AIMXVI". 

External links[edit]