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.

## 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 July 16, 2019 at 18:34:08. See the history of this page for a list of all contributions to it.