Agda theorem prover
Encyclopedia
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
for developing constructive proof
Constructive proof
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...
s based on the Curry-Howard correspondence in a variant of Per Martin-Löf
Per Martin-Löf
Per Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in...
's Type Theory
Intuitionistic type theory
Intuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
. It can also be seen as a functional programming language with dependent type
Dependent type
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram....
s. Agda was developed by Ulf Norell, a postdoctoral researcher at Chalmers University of Technology
Chalmers University of Technology
Chalmers University of Technology , is a Swedish university located in Gothenburg that focuses on research and education in technology, natural science and architecture.-History:...
.
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
Emacs
Emacs is a class of text editors, usually characterized by their extensibility. GNU Emacs has over 1,000 commands. It also allows the user to combine these commands into macros to automate work.Development began in the mid-1970s and continues actively...
interface and a graphical interface, Alfa.
Agda 2
The current version of Agda, Agda 2, has been developed at Chalmers by Ulf Norell. The syntax has changed from Agda 1 (though some conversion tools are being developed as well), introducing for instance, implicit variables that can be omitted when deducible from the context. Agda 2 also makes extensive use of UnicodeUnicode
Unicode is a computing industry standard for the consistent encoding, representation and handling of text expressed in most of the world's writing systems...
as a way to obtain easily readable proofs.
Agda 2 provides either a commandline tool or a powerful Emacs
Emacs
Emacs is a class of text editors, usually characterized by their extensibility. GNU Emacs has over 1,000 commands. It also allows the user to combine these commands into macros to automate work.Development began in the mid-1970s and continues actively...
mode, developed by Makoto Takeyama and Nils Anders Danielsson.
The 10th Agda Implementor's Meeting was held in Gothenburg
Gothenburg
Gothenburg is the second-largest city in Sweden and the fifth-largest in the Nordic countries. Situated on the west coast of Sweden, the city proper has a population of 519,399, with 549,839 in the urban area and total of 937,015 inhabitants in the metropolitan area...
in September 2009. AIM11 is scheduled for March in Japan
Japan
Japan is an island nation in East Asia. Located in the Pacific Ocean, it lies to the east of the Sea of Japan, China, North Korea, South Korea and Russia, stretching from the Sea of Okhotsk in the north to the East China Sea and Taiwan in the south...
.
Agda 2 is similar to Epigram.
External links
- The Agda 2 homepage (a wiki), including documentation and a link to a bug-report tool
- Agda at the Hackage repository
- Learn you an Agda, a tutorial.
- A course on Functional Programming, with seven parts on Agda
- Introduction to Agda, a five-part YouTube playlist by Daniel Peebles
- Dependently Typed Programming in Agda, by Ulf Norell
- A Brief Overview of Agda, by Ana Bove, Peter Dybjer, and Ulf Norell
- An Agda Tutorial, Misao Nagayama, Hideaki Nishihara, Makoto Takeyam (2006)