A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Logic in Computer Science
2015-07-01 v3
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.
Cite
@article{arxiv.1102.2405,
title = {A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance},
author = {Andreas Abel and Thierry Coquand and Miguel Pagano},
journal= {arXiv preprint arXiv:1102.2405},
year = {2015}
}