Agda (programming language)

Not to be confused with the programming language Ada.

Agda
A stylized chicken in black lines and dots, to the left of the name "Agda" in sans-serif test with the first letter slanted to the right.
ParadigmFunctional
Designed byUlf Norell; Catarina Coquand (1.0)
DeveloperChalmers University of Technology
First appeared1.0 – 1999; 25 years ago (1999)
2.0 – 2007; 17 years ago (2007)
Stable release
2.7.0 / August 16, 2024; 50 days ago (2024-08-16)
Typing disciplinestrong, static, dependent, nominal, manifest, inferred
Implementation languageHaskell
OSCross-platform
LicenseBSD-like[1]
Filename extensions.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
Websitewiki.portal.chalmers.se/agda
Influenced by
Coq, Epigram, Haskell
Influenced
Idris

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis.[2] The original Agda system was developed at Chalmers by Catarina Coquand in 1999.[3] The current version, originally named Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.

Agda is also a proof assistant based on the propositions-as-types paradigm (Curry–Howard correspondence), but unlike Coq, has no separate tactics language, and proofs are written in a 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 Emacs, Atom, and VS Code interfaces[4][5][6] but can also be run in batch processing mode from a command-line interface.

Agda is based on Zhaohui Luo's unified theory of dependent types (UTT),[7] a type theory similar to Martin-Löf type theory.

Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk,[8] which is about a hen named Agda. This alludes to the name of the theorem prover Coq, which was named after Thierry Coquand.

  1. ^ Agda license file
  2. ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1]
  3. ^ "Agda: An Interactive Proof Editor". Archived from the original on 8 October 2011. Retrieved 20 October 2014.
  4. ^ Coquand, Catarina; Synek, Dan; Takeyama, Makoto (2005). An Emacs interface for type directed support constructing proofs and programs (PDF). European Joint Conferences on Theory and Practice of Software 2005. Archived from the original (PDF) on 22 July 2011.
  5. ^ "agda-mode on Atom". Retrieved 7 April 2017.
  6. ^ "agda-mode - Visual Studio Marketplace". marketplace.visualstudio.com. Retrieved 6 June 2023.
  7. ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
  8. ^ "[Agda] origin of "Agda"? (Agda mailing list)". Retrieved 24 October 2020.