Agda (programming language)
Functional programming language / From Wikipedia, the free encyclopedia
Dear Wikiwand AI, let's keep it short by simply answering these key questions:
Can you list the top facts and stats about Agda (programming language)?
Summarize this article for a 10 year old
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 known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.
Paradigm | Functional |
---|---|
Designed by | Ulf Norell; Catarina Coquand (1.0) |
Developer | Ulf Norell; Catarina Coquand (1.0) |
First appeared | 2007; 17 years ago (2007) (1.0 in 1999; 25 years ago (1999)) |
Stable release | 2.6.3
/ January 30, 2023; 15 months ago (2023-01-30) |
Typing discipline | strong, static, dependent, nominal, manifest, inferred |
Implementation language | Haskell |
OS | Cross-platform |
License | BSD-like[1] |
Filename extensions | .agda , .lagda , .lagda.md , .lagda.rst , .lagda.tex |
Website | wiki |
Influenced by | |
Coq, Epigram, Haskell | |
Influenced | |
Idris |
Agda is also a proof assistant based on the propositions-as-types paradigm, 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 mode from the command line.
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.