Benjamin Werner - On the strength of proof-irrelevant type theories

lmcs:1142 - Logical Methods in Computer Science, September 26, 2008, Volume 4, Issue 3 - https://doi.org/10.2168/LMCS-4(3:13)2008
On the strength of proof-irrelevant type theories

Authors: Benjamin Werner

    We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics.


    Volume: Volume 4, Issue 3
    Published on: September 26, 2008
    Accepted on: June 25, 2015
    Submitted on: February 13, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.1

    Linked data

    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 ;

    9 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 576 times.
    This article's PDF has been downloaded 257 times.