pisigma

A dependently typed core language.

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.