The uAgda package

[Tags: program]

uAgda implements an experimental dependently-typed language (and proof assistant by the Curry-Howard isomorphism). The goal of the project is twofold:

1. Experiment with a minimalistic language that is strong enough to program and reason in.

2. Give a simple implementation of its type-checker (ours is ~200 lines).

See the share/tutorial directory for how to get started.


Dependenciesbase (==4.*), BNFC-meta (==0.1.*), cmdargs (==0.6.*), containers (==0.3.*), monads-fd (==0.1.*), parsec (==2.1.*), pretty (==1.0.*), transformers (==0.2.*)
AuthorJean-Philippe Bernardy
CategoryDependent Types
UploadedThu Dec 2 15:11:34 UTC 2010 by JeanPhilippeBernardy
Downloads707 total (61 in last 30 days)
StatusDocs pending
Build status unknown [no reports yet]


Maintainers' corner

For package maintainers and hackage trustees