Agda (programming language)

Common card · No. 332789

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). Proofs are formulated in a purely functional programming style, and constructed either by hand or by meta-programming ("reflection"). 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...

Read on Wikipedia · Image The Agda Community / Miëtek Bak, BSD