{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:18Z","timestamp":1761611238033},"reference-count":8,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4573,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1996,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a short and direct syntactic proof of the fact that adding the axiom of choice and the principle of excluded-middle to Coquand\u2013Huet's Calculus of Constructions gives proof-irrelevance.<\/jats:p>","DOI":"10.1017\/s0956796800001829","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:10:59Z","timestamp":1226056259000},"page":"519-526","source":"Crossref","is-referenced-by-count":8,"title":["Proof-irrelevance out of excluded-middle and choice in the calculus of constructions"],"prefix":"10.1017","volume":"6","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Berardi","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001829_ref005","unstructured":"Geuvers H. (1993) Logics and Type Systems. PhD Thesis, University of Nijmegen."},{"key":"S0956796800001829_ref003","volume-title":"Logic and Computer Science","author":"Coquand","year":"1990"},{"key":"S0956796800001829_ref002","unstructured":"Berardi S. (1994) A formalization in LEGO of a proof of CC+\\epsilon\\mathcal{M}+\\mathcal{A}\\mathcal{C}\\vdash Proof-Irrelevance. Technical Report, Department of Computer Science University of Torino."},{"key":"S0956796800001829_ref001","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"S0956796800001829_ref008","unstructured":"Pottinger G. (1989) Definite descriptions and excluded middle in the calculus of constructions. TYPES network, November."},{"key":"S0956796800001829_ref006","doi-asserted-by":"crossref","unstructured":"Geuvers H. (1994) Conservativity between logics and typed \u03bb-calculi. Proc. BRA Workshop on Types for Proofs and Programs.","DOI":"10.1007\/3-540-58085-9_73"},{"key":"S0956796800001829_ref007","unstructured":"Hurkens A. J. C. (1995) A simplification of Girard's paradox. In Dezani-Ciancaglini M. and Plotkin G. editors, Proc. 2nd International Conference on Typed Lambda Calculi and Applications (TLCA'95): Lecture Notes in Computer Science 902.Springer-Verlag."},{"key":"S0956796800001829_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001829","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T17:40:47Z","timestamp":1557682847000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001829\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,5]]},"references-count":8,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1996,5]]}},"alternative-id":["S0956796800001829"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001829","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,5]]}}}