natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
A dependently typed functional programming language with applications to certified programming. It is also used as a proof assistant.
Besides Coq, Agda is one of the languages in which homotopy type theory has been implemented (Brunerie). Agda can be compiled to Haskell, Epic or Javascript.
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
Historical projects that died out:
General information on Agda is at
Ulf Norell, James Chapman, Dependently Typed Programming in Agda (pdf)
Dan Licata, Ian Voysey, Programming and proving in Agda
Ulf Norell, Towards a practical programming
language based on dependent type theory_, 2007 (pdf)
A tutorial for use of Agda as an implementation of homotopy type theory is at
Guillaume Brunerie, Agda for homotopy type theory (web)
Guillaume Brunerie, The Agda proof assistant, slides, pdf
and specifically of Cubical Agda as an implementation of cubical type theory:
The HoTT-Agda library is at
Last revised on September 12, 2019 at 03:04:06. See the history of this page for a list of all contributions to it.