Agda
This page is outdated. For an up-to-date description of Agda see the
Agda Wiki page
Agda is a system for incrementally developing proofs and programs. Agda
is also a functional language with dependent types. This language is
very similar to cayenne
and agda is intended to be a (almost) full implementation of it in the
future.
* The pages below are modifications
of the description of cayenne.
Catarina Coquand
Last modified: Sun Feb 27 10:22:44 MET 2000