# 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 implementsed (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

category: software

Revised on December 29, 2015 10:54:33 by Bas Spitters (87.104.153.152)