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 March 20, 2013 16:56:42 by Zoran Škoda (161.53.130.104)