Sciweavers

Share
CADE
2006
Springer

On the Strength of Proof-Irrelevant Type Theories

9 years 8 months ago
On the Strength of Proof-Irrelevant Type Theories
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.
Benjamin Werner
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where CADE
Authors Benjamin Werner
Comments (0)
books