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

The HoTT-Agda library is at

category: software

Last revised on April 8, 2019 at 10:44:20. See the history of this page for a list of all contributions to it.