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
    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

    6 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 3018 times.
    This article's PDF has been downloaded 501 times.