Agda: An Interactive Proof Editor

This is the homepage for Agda version 1.

For information on the current Agda version 2,
please visit Agda Wiki page: http://wiki.portal.chalmers.se/agda/

Overview

Agda is an interactive proof editor, or proof assistant, developed in Chalmers University of Technology, in the tradition of succession of such proof assistants (ALF, Cayenne, Alfa).  Its input language, called Agda language (or simply Agda), is based on a constructive type theory á la Martin-Löf, extended with dependent record types, inductive definitions, module structures and a class hierarchy mechanism.


The notion of dependent record types *[BT, CPT] is an extension of dependent products which takes field names into account.  Dependent record types in Agda are called signatures, thus given the keyword "sig".  Dependent records (i.e., values of signatures), are structures; they have the keyword "struct".

Inductive definitions in Agda start with the keyword "data", and follow the form of data type definition a la functional programming languages such as Haskell and ML.  A more powerful means of inductive definition starting with the keyword "idata" is also provided.

Modules are called "packages".  Identifiers are imported by "use" declarations.  No definitions are opaque; all identifiers defined in a package are exported from a package.

The class mechanism of Agda is similar to that of Haskell.

Agda language is emerging.  Its first form, as reported in Catarina Coquand's home page, should now be called Agda1/OldSyntax. The users should now use its successor, Agda1/NewSyntax, which is available since the summer of 2005.  The new syntax gives, for instance, easier control to asking for explicit or implicit specification of actual parameters in functional value definitions.  A definition of Agda1/NewSyntax in pseudo BNF will be given here(under construction), and an example, which should, for the moment, work as a quick tutorial for beginners, will be available here.

A research development of Agda2 language and its interactive proof editor, which is also called Agda2, is going on.  Although Agda2 would eventually replace Agda1 and would be `the' Agda, we at least tentatively call it Agda2.  It is because both the language and its proof editor are still in alpha test phase, so most users are expected to use Agda1/NewSyntax.  Of course those who are willing to contribute to the alpha test are invited to use Agda2 as it is, and to give suggestions for improvement.

Agda with its emacs-based interface are distributed freely as an open source software under the MIT / Expat license.


*[BT]     G. Betarte and A. Tasistro.
            Extension of Martin-Löf's Type Theory with Record Types and Subtyping.
            25 Years of Constructive Type Theory, Oxford University Press, 1998.

*[CPT]     Thierry Coquand, Randy Pollack, and Makoto Takeyama.
                A Logical Framework with Dependently Typed Records.
                Fundamenta Informaticae, vol. 65(1-2), pp. 113--134, 2005.