Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs based on the Curry-Howard correspondence in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types. Agda was developed by Ulf Norell, a postdoctoral researcher at Chalmers University of Technology.
Agda is based on ...
More
Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs based on the Curry-Howard correspondence in a variant of Per Martin-Löf's Type Theory. It can also be seen as a functional programming language with dependent types. Agda was developed by Ulf Norell, a postdoctoral researcher at Chalmers University of Technology.
Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script. The language has ordinary programming constructs such as data-types and case-expressions, signatures and records, let-expressions and modules. The system has an Emacs interface and a graphical interface, Alfa.
As a programming language, Agda has Haskell-like syntax, and the Agda 2 compiler can convert Agda proofs into functions in the Haskell, JavaScript, or Epic languages.
The current version of Agda, Agda 2, has been developed at Chalmers by...
Less
