@inproceedings{a6478c911299485aa03ac0ffd9347d53,
title = "On the strength of proof-irrelevant type theories",
abstract = "We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is particularly 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. Finally 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.",
author = "Benjamin Werner",
year = "2006",
month = jan,
day = "1",
doi = "10.1007/11814771\_49",
language = "English",
isbn = "3540371877",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "604--618",
booktitle = "Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings",
note = "Third International Joint Conference on Automated Reasoning, IJCAR 2006 ; Conference date: 17-08-2006 Through 20-08-2006",
}