{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:39:34Z","timestamp":1770291574714,"version":"3.49.0"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,9,26]],"date-time":"2008-09-26T00:00:00Z","timestamp":1222387200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a type theory with some proof-irrelevance built into the\nconversion rule. We argue that this feature is useful when type theory is used\nas the logical formalism underlying a theorem prover. We also show a close\nrelation with the subset types of the theory of PVS. We show that in these\ntheories, because of the additional extentionality, the axiom of choice implies\nthe decidability of equality, that is, almost classical logic. Finally we\ndescribe a simple set-theoretic semantics.<\/jats:p>","DOI":"10.2168\/lmcs-4(3:13)2008","type":"journal-article","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T10:23:46Z","timestamp":1231496626000},"source":"Crossref","is-referenced-by-count":11,"title":["On the strength of proof-irrelevant type theories"],"prefix":"10.46298","volume":"Volume 4, Issue 3","author":[{"given":"Benjamin","family":"Werner","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,9,26]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1142\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1142\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:04:28Z","timestamp":1681243468000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9,26]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(3:13)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0808.3928","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0808.3928","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,9,26]]},"article-number":"1142"}}