Lambda the Ultimate

An article (draft) titled "ΠΣ: A Core Language for Dependently Typed Programming", an online demo and a Hackage repository with source code for a type checker.

To my big surprise I haven't found it on LtU.

This is a proposal for a language that could serve the role the Haskell Core serves for Haskell - a small in list of features, verbose language in which we can translate higher-level concepts.

This is interesting as PiSigma contains minimum features and one can play with implementation.