pisigma

A dependently typed core language

Latest on Hackage:0.2.1

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

PiSigma is a small dependently typed language with only very few constructs: Type:Type, Pi-types, Sigma-types, enumerations and a general meachanism for mutual recursion for types and values controlled by lifted types. It is intended as a core language for dependently typed languages like Agda. It has been described in the paper emPiSigma: Dependent Types Without the Sugar/em which has appeared in the proceedings of FLOPS 2010.