On the strength of proof-irrelevant type theories

Benjamin Werner

doi:10.2168/LMCS-4(3:13)2008

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 theoriesArticle

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.

Comment: 20 pages, Logical Methods in Computer Science, Long version of IJCAR 2006 paper

https://doi.org/10.2168/LMCS-4(3:13)2008

Source: arXiv.org:0808.3928

Volume: Volume 4, Issue 3

Secondary volumes: Selected Papers of the 3rd International Joint Conference on Automated Reasoning (IJCAR 2006)

Published on: September 26, 2008

Imported on: February 13, 2007

Keywords: Computer Science - Logic in Computer Science, F.4.1, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

12 Documents citing this article

Yiyun Liu;Jonathan Chan;Stephanie Weirich, 2025, Consistency of a Dependent Calculus of Indistinguishability, Proceedings of the ACM on Programming Languages, 9, POPL, pp. 183-209, 10.1145/3704843, https://doi.org/10.1145/3704843.

Loïc Pujet;Nicolas Tabareau, 2024, Observational Equality Meets CIC, Lecture notes in computer science, pp. 275-301, 10.1007/978-3-031-57262-3_12, https://doi.org/10.1007/978-3-031-57262-3_12.

Hondet, Gabriel;Blanqui, Frédéric, 2021, Encoding of Predicate Subtyping with Proof Irrelevance in the $λ$$Π$-Calculus Modulo Theory, DROPS (Schloss Dagstuhl – Leibniz Center for Informatics), 10.4230/lipics.types.2020.6, https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.6.

Richard Dapoigny;Patrick Barlatier, 2013, Modeling Ontological Structures with Type Classes in Coq, Lecture notes in computer science, pp. 135-152, 10.1007/978-3-642-35786-2_11.

Andreas Abel;Gabriel Scherer, 2012, On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, Volume 8, Issue 1, 10.2168/lmcs-8(1:29)2012, https://doi.org/10.2168/lmcs-8(1:29)2012.

Zhaohui Luo, 2012, Common Nouns as Types, Lecture notes in computer science, pp. 173-185, 10.1007/978-3-642-31262-5_12.

Andreas Abel, 2011, Irrelevance in Type Theory with a Heterogeneous Equality Judgement, Lecture notes in computer science, pp. 57-71, 10.1007/978-3-642-19805-2_5.

Andreas Abel;Thierry Coquand;Miguel Pagano, 2011, A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance, Logical Methods in Computer Science, Volume 7, Issue 2, 10.2168/lmcs-7(2:4)2011, https://doi.org/10.2168/lmcs-7(2:4)2011.

Gyesik Lee;Benjamin Werner, 2011, Proof-irrelevant model of CC with predicative induction and judgmental equality, Logical Methods in Computer Science, Volume 7, Issue 4, 10.2168/lmcs-7(4:5)2011, https://doi.org/10.2168/lmcs-7(4:5)2011.

Richard Dapoigny;Patrick Barlatier, 2011, Using a Dependently-Typed Language for Expressing Ontologies, Lecture notes in computer science, pp. 257-268, 10.1007/978-3-642-25975-3_23.

Daria Walukiewicz-Chrząszcz;Jacek Chrząszcz, 2010, Inductive Consequences in the Calculus of Constructions, Lecture notes in computer science, pp. 450-465, 10.1007/978-3-642-14052-5_31.

Andreas Abel;Thierry Coquand;Miguel Pagano, 2009, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Lecture notes in computer science, pp. 5-19, 10.1007/978-3-642-02273-9_3.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3541 times.

This article's PDF has been downloaded 741 times.