Proof assistants based on Martin-Löf's type theory have been developed in Gothenburg since 1983. The first system was an implemetation written by Kent Petersson of the extensional version of Martin-Löf type theory. This system was based on the Edinburgh LCF system.
Systems based on Martin-Löf's logical framework and the intensional versions of Martin-Löf type theory have been developed in Gothenburg since around 1990. The first was called ALF (A Logical Framework). The type checker was written by Thierry Coquand and the window interface was written by Lennart Augutsson based on Bengt Nordström's ideas of designing a "proof editor" for Martin-Löf type theory, where the user builds proofs by pointing and clicking and with place holders. A second version of ALF was written by Lena Magnusson. It is described in the papers
In the mid 1990s it was time for a redesign. First a prototype was implemented in gofer (1995)
- Half: general description.
Here is a simple example (an inductive representation of a coinductive notion) in this system. Note the "theory mechanism" inspired from PVS.
A version in C was implemented by Dan Synek (1996). See the PhD thesis of Jan Cederquist for some examples.
Catarina Coquand implemented then in Haskell the original version of Agda ("Agda 1") following the design pattern of half. See also this article which is the source of the current emacs interface.
Thomas Hallgren wrote an advanced window interface for Agda:
A closely related system which was instead aimed for the functional programming community was Cayenne. This language and its compiler were designed and implemented by Lennart Augustsson.
In 2004 the Programming Logic Group began collaborating with the Centre for Verification and Semantics at AIST in Amagasaki on the development and application of Agda. At this time the Agda Implementors Meetings (AIMs) started with biannual meetings alternating between Sweden and Japan.
In 2005 work began on a new version of Agda, and a prototype named AgdaLight was written by Ulf Norell and Andreas Abel. Shortly thereafter work on the design and implementation of the current Agda system ("Agda 2") began. A main reference is the thesis of Ulf Norell.
- Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.