Back to Search
Start Over
On the strength of proof-irrelevant type theories
- Source :
- Logical Methods in Computer Science, Volume 4, Issue 3 (September 26, 2008) lmcs:1142
- Publication Year :
- 2008
-
Abstract
- 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.<br />Comment: 20 pages, Logical Methods in Computer Science, Long version of IJCAR 2006 paper
- Subjects :
- Computer Science - Logic in Computer Science
F.4.1
F.3.1
Subjects
Details
- Database :
- arXiv
- Journal :
- Logical Methods in Computer Science, Volume 4, Issue 3 (September 26, 2008) lmcs:1142
- Publication Type :
- Report
- Accession number :
- edsarx.0808.3928
- Document Type :
- Working Paper
- Full Text :
- https://doi.org/10.2168/LMCS-4(3:13)2008