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 the intensional versions of dependent 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. The implementation was relying on type-checking with a list of constraints on metavariables, see the description in this paper
A second version of ALF was written by Lena Magnusson. It is described in the papers
- ALF: general description, user's guide.
In the mid 1990s it was time for a redesign. First a prototype was implemented in gofer (1995) by Coquand. 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. Here is example of a proof in this system and here is Conor McBride's lecture at the TYPES summer school 2005, which also uses this system.
- This is described on the AIST Agda page http://ocvs.cfv.jp/Agda/index.html and on the sf.net page
Thomas Hallgren wrote an advanced window interface for Agda:
Here is an example of a proof in this system.
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.