Logical Methods in Computer Science (May 2011)

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

  • Andreas Abel,
  • Thierry Coquand,
  • Miguel Pagano

DOI
https://doi.org/10.2168/LMCS-7(2:4)2011
Journal volume & issue
Vol. Volume 7, Issue 2

Abstract

Read online

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.

Keywords