Contents

# Contents

## Overview

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.

proof assistants:

based on plain type theory/set theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

## References

General information on Agda is at

A tutorial for use of Agda as an implementation of homotopy type theory is at

and specifically of Cubical Agda as an implementation of cubical type theory:

The HoTT-Agda library is at

category: software

Last revised on September 12, 2019 at 03:04:06. See the history of this page for a list of all contributions to it.