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. 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
- Half: general description.
This version did not include an Identity type. A version in C was implemented by Dan Synek (1996). See the PhD thesis of Jan Cederquist for some examples.
Based on these ideas Catarina Coquand implemented the original version of Agda (“Agda 1″).
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. 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.