A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel, Thierry Coquand, Miguel Pagano

We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluati…