Agda

Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program.

Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram, Matita and NuPRL.

Agda is open-source and enjoys contributions from many authors. The center of the Agda development is the Programming Logic group at Chalmers and Gothenburg University; the main developers are Ulf Norell, Nils Anders Danielsson, and Andreas Abel.

Agda meetings

Agda users and implementors meet biannually for a week of talks and code sprints.

  • The next Agda meeting, AIM XXVI, will held at Eötvös Loránd University in Budapest, Hungary, Monday 29th of January to Saturday 3rd of February 2018.
  • Past Agda Meetings.

News

  • (2017-09-11) The standard library 0.14 is now available.
  • (2017-09-08) Agda 2.5.3 is now available.
  • (2016-12-22) The standard library 0.13 is now available.
  • (2016-12-22) Agda 2.5.2 is now available.
  • (2016-11-25) Agda 2.5.1.2 is now available.
  • (2016-06-21) Agda 2.5.1.1 is now available.
  • (2016-04-16) The standard library 0.12 is now available.
  • (2016-04-16) Agda 2.5.1 is now available.
  • (2015-12-18) Agda 2.4.2.5 is now available.
  • (2015-10-28) The standard library 0.11 is now available.
  • (2015-09-26) Agda 2.4.2.4 is now available.
  • (2015-09-25) The standard library 0.10 is now available.
  • (2015-05-25) Agda 2.4.2.3 is now available.
  • (2014-11-26) Agda 2.4.2.2 is now available.
  • (2014-11-14) The standard library 0.9 is now available.
  • (2014-11-14) Agda 2.4.2.1 is now available.
  • (2014-08-29) The standard library 0.8.1 is now available.
  • (2014-08-29) Agda 2.4.2 is now available.
  • (2014-07-29) Agda 2.4.0.2 is now available.
  • (2014-06-20) Agda 2.4.0.1 is now available.

Getting started

Documentation and examples

Further information

Old/outdated stuff