Andreas Abel ; Thierry Coquand ; Miguel Pagano - 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 - https://doi.org/10.2168/LMCS-7(2:4)2011
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof IrrelevanceArticle

Authors: Andreas Abel ; Thierry Coquand ; Miguel Pagano

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.

https://doi.org/10.2168/LMCS-7(2:4)2011
Source: arXiv.org:1102.2405
Volume: Volume 7, Issue 2
Secondary volumes: Selected Papers of the 9th Conference on Typed Lambda Calculi and Applications (TLCA 2009)
Published on: May 7, 2011
Imported on: November 15, 2009
Keywords: Computer Science - Logic in Computer Science, F.4.1
Licence: arXiv.org - Non-exclusive license to distribute

8 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3296 times.
This article's PDF has been downloaded 556 times.