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 Irrelevance

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.


    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

    Linked publications - datasets - softwares

    Source : ScholeXplorer IsCitedBy ARXIV 2110.13704
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.types.2020.6
    • 10.4230/lipics.types.2020.6
    • 2110.13704
    Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
    Hondet, Gabriel ; Blanqui, Frédéric ;

    4 Documents citing this article

    Consultation statistics

    This page has been seen 728 times.
    This article's PDF has been downloaded 234 times.