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
UploadedFri Dec 3 10:15:16 UTC 2010 by JeanPhilippeBernardy
Downloads717 total (53 in last 30 days)
StatusDocs pending
Build status unknown [no reports yet]


Maintainers' corner

For package maintainers and hackage trustees