{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T12:46:11Z","timestamp":1745325971845},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_49","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"604-618","source":"Crossref","is-referenced-by-count":6,"title":["On the Strength of Proof-Irrelevant Type Theories"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Werner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"49_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"T. Altenkirch","year":"1994","unstructured":"Altenkirch, T.: Proving strong normalization for CC by modifying realizability semantics. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, Springer, Heidelberg (1994)"},{"doi-asserted-by":"crossref","unstructured":"Altenkirch, T.: Extensional Equality in Intensional Type Theory. LICS (1999)","key":"49_CR2","DOI":"10.1109\/LICS.1999.782636"},{"doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Lambda Calculi with Types.Technical Report 91-19, Catholic University Nijmegen, 1991.In Handbook of Logic in Computer Science, Vol II, Elsevier (1992)","key":"49_CR3","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"49_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"755","DOI":"10.1007\/BFb0055099","volume-title":"Automata, Languages and Programming","author":"G. Barthe","year":"1998","unstructured":"Barthe, G.: The relevance of proof-irrelevance. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 755\u2013768. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. MSCS, vol.\u00a015(1) (2003)","key":"49_CR5","DOI":"10.1017\/S0960129504004426"},{"key":"49_CR6","volume-title":"Proceedings of the 12th IEEE International Conference on Automated Software Engineering","author":"J. Caldwell","year":"1997","unstructured":"Caldwell, J.: Moving Proofs-as-Programs into Practice. In: Proceedings of the 12th IEEE International Conference on Automated Software Engineering, IEEE, Los Alamitos (1997)"},{"doi-asserted-by":"crossref","unstructured":"Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ICFP 2005 (2005)","key":"49_CR7","DOI":"10.1145\/1086365.1086375"},{"unstructured":"The Coq Development Team. The Coq Proof-Assistant User\u2019s Manual, INRIA, http:\/\/coq.inria.fr\/","key":"49_CR8"},{"key":"49_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_39","volume-title":"Computer Science Logic","author":"P. Courtieu","year":"2001","unstructured":"Courtieu, P.: Normalized Types. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, Springer, Heidelberg (2001)"},{"unstructured":"Gimenez, E.: A Tutorial on Recursive Types in Coq. INRIA Technical Report (1999)","key":"49_CR10"},{"unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem. Manuscript (2005)","key":"49_CR11"},{"doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: proceedings of ICFP (2002)","key":"49_CR12","DOI":"10.1145\/581478.581501"},{"unstructured":"Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml. Th\u00e9se de doctorat, Universit\u00e9 Paris 7 (2003)","key":"49_CR13"},{"key":"49_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Functional and Logic Programming","author":"L. Th\u00e9ry","year":"2006","unstructured":"Th\u00e9ry, L., Werner, B., Gr\u00e9goire, B.: A computational approach to Pocklington certificates in type theory. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol.\u00a03945, Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: A groupoid model refutes uniqueness of identity proofs. LICS 1994, Paris (1994)","key":"49_CR15","DOI":"10.1109\/LICS.1994.316071"},{"doi-asserted-by":"crossref","unstructured":"Luo, Z.: ECC: An Extended Calculus of Constructions. In: Proc. of IEEE LICS 1989 (1989)","key":"49_CR16","DOI":"10.1109\/LICS.1989.39193"},{"unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory. Studies in Proof Theory, Bibliopolis (1984)","key":"49_CR17"},{"key":"49_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C. McBride","year":"2002","unstructured":"McBride, C.: Elimination with a Motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, Springer, Heidelberg (2002)"},{"key":"49_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037113","volume-title":"Typed Lambda Calculi and Applications","author":"J. McKinna","year":"1993","unstructured":"McKinna, J., Pollack, R.: Pure Type Systems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, Springer, Heidelberg (1993)"},{"key":"49_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097796","volume-title":"Types for Proofs and Programs","author":"P.-A. Melli\u00e8s","year":"1998","unstructured":"Melli\u00e8s, P.-A., Werner, B.: A Generic Normalization Proof for Pure Type System. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, Springer, Heidelberg (1998)"},{"key":"49_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_14","volume-title":"Types for Proofs and Programs","author":"A. Miquel","year":"2003","unstructured":"Miquel, A., Werner, B.: The not so simple proof-irrelevant model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Nogin, A., Kopilov, A.: Formalizing Type Operations Using the Image Type Constructor. In: WoLLIC. ENTCS (to appear, 2006)","key":"49_CR22","DOI":"10.1016\/j.entcs.2006.05.041"},{"unstructured":"Owre, S., Shankar, N.: The Formal Semantics of PVS. SRI Technical Report CSL-97-2R. Revised (March 1999)","key":"49_CR23"},{"unstructured":"Paulin-Mohring, C.: Extraction de Programmes dans le Calcul des Constructions. Th\u00e8se de doctorat, Universit\u00e9 Paris 7 (1989)","key":"49_CR24"},{"key":"49_CR25","volume-title":"Proceedings of LICS","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In: Proceedings of LICS, IEEE, Los Alamitos (2001)"},{"key":"49_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014566","volume-title":"Theoretical Aspects of Computer Software","author":"B. Werner","year":"1997","unstructured":"Werner, B.: Sets in Types, Types in Sets. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, Springer, Heidelberg (1997)"},{"unstructured":"Hongwei Xi, Dependent Types in Practical Programming, Ph.D, CMU (1998)","key":"49_CR27"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,7]],"date-time":"2024-02-07T00:48:42Z","timestamp":1707266922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11814771_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}