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

TL;DR

This paper introduces a modular type-checking algorithm for a type theory featuring singleton types and proof irrelevance, supported by a PER model and normalization-by-evaluation, with proven correctness and completeness.

Contribution

It presents a novel modular algorithm for type checking in a type theory with singleton types and proof irrelevance, including formal semantics and correctness proofs.

Findings

Correctness and completeness of the type-checking algorithm

Injectivity of type constructors proven

Extension to proof-irrelevant propositions achieved

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.