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

Abstract

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-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.

References in corpus (1)

• On the strength of proof-irrelevant type theories

Cited by in corpus (4)

• On Irrelevance and Algorithmic Equality in Predicative Type Theory
• Efficient Extensional Binary Tries
• Staged Compilation with Two-Level Type Theory
• Confluent terminating extensional lambda-calculi with surjective pairing and terminal type