# 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

• Guillaume Brunerie, The Agda proof assistant, slides, pdf

category: software

Revised on June 18, 2013 09:51:19 by Urs Schreiber (82.113.106.200)