A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Andreas Abel, Thierry Coquand, Miguel Pagano
Source record
Source: Crossref
Published: May 7, 2011
DOI: 10.2168/lmcs-7(2:4)2011
Open original source ↗Source 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.
Evidence graph
No public relationships recorded yet.
Integrity note: This page is a factual metadata record created by deterministic ingestion. It is not a claim that the work moves a mathematical frontier or has been independently verified.