Agda (programming language)

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. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. 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 Rocq, 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 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), a type theory similar to Martin-Löf type theory. Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk, which is about a hen named Agda. This alludes to the name of the theorem prover Rocq, which was originally named Coq after Thierry Coquand.