uAgda

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.