The uAgda package
uAgda implements an experimental dependently-typed language (and proof assistant by the Curry-Howard isomorphism), extended with support for parametricity.
See the share/tutorial directory for how to get started.
Properties
| Versions | 1.0.0.0, 1.0.0.1, 1.0.0.2, 1.1.0.0, 1.2.0.0, 1.2.0.1, 1.2.0.2, 1.2.0.3, 1.2.0.4 |
|---|---|
| Dependencies | array (0.3.*), base (4.*), BNFC-meta (0.2.*), cmdargs (0.6.*), containers (0.4.*), mtl (2.0.*), parsec (2.1.*), pretty (1.1.*), split (0.1.*), transformers (0.2.*) |
| License | OtherLicense |
| Author | Jean-Philippe Bernardy |
| Maintainer | jeanphilippe.bernardy@gmail.com |
| Category | Dependent Types |
| Executables | uAgda |
| Upload date | Sat Mar 10 08:38:04 UTC 2012 |
| Uploaded by | JeanPhilippeBernardy |
Downloads
- uAgda-1.2.0.3.tar.gz (Cabal source package)
- package description (included in the package)