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

We define a logical framework with singleton types and one universe of smalltypes. We give the semantics using a PER model; it is used for constructing anormalisation-by-evaluation algorithm. We prove completeness and soundness ofthe algorithm; and get as a corollary the injectivity of type constructors.Then we give the definition of a correct and complete type-checking algorithmfor terms in normal form. We extend the results to proof-irrelevantpropositions