Abel, Andreas and Coquand, Thierry and Pagano, Miguel - A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

lmcs:1069 - Logical Methods in Computer Science, May 7, 2011, Volume 7, Issue 2
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Authors: Abel, Andreas and Coquand, Thierry and Pagano, Miguel

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.


Source : oai:arXiv.org:1102.2405
DOI : 10.2168/LMCS-7(2:4)2011
Volume: Volume 7, Issue 2
Published on: May 7, 2011
Submitted on: November 15, 2009
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 76 times.
This article's PDF has been downloaded 17 times.