{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:49:15Z","timestamp":1725533355221},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642024436"},{"type":"electronic","value":"9783642024443"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02444-3_3","type":"book-chapter","created":{"date-parts":[[2009,6,6]],"date-time":"2009-06-06T05:15:35Z","timestamp":1244265335000},"page":"32-48","source":"Crossref","is-referenced-by-count":2,"title":["A New Elimination Rule for the Calculus of Inductive Constructions"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Corbineau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge Luis","family":"Sacchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"The Coq Development\u00a0Team. The Coq Reference Manual, version 8.1. Distributed electronically (February 2007), \n                  \n                    http:\/\/coq.inria.fr\/doc"},{"key":"3_CR2","unstructured":"Coquand, T.: Pattern matching with dependent types. In: Nordstr\u00f6m, B., Petersson, K., Plotkin, G. (eds.) Informal Proceedings Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden (1992)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/11780274_27","volume-title":"Algebra, Meaning, and Computation","author":"H. Goguen","year":"2006","unstructured":"Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol.\u00a04060, pp. 521\u2013540. Springer, Heidelberg (2006)"},{"key":"3_CR4","first-page":"208","volume-title":"LICS","author":"M. Hofmann","year":"1994","unstructured":"Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: LICS, pp. 208\u2013212. IEEE Computer Society, Los Alamitos (1994)"},{"key":"3_CR5","unstructured":"McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/11546382_3","volume-title":"Advanced Functional Programming","author":"C. McBride","year":"2005","unstructured":"McBride, C.: Epigram: Practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol.\u00a03622, pp. 130\u2013170. Springer, Heidelberg (2005)"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program.\u00a014(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"3_CR8","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology (2007)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/1292597.1292606","volume-title":"PLPV","author":"N. Oury","year":"2007","unstructured":"Oury, N.: Pattern matching coverage checking with dependent types using set approximations. In: Stump, A., Xi, H. (eds.) PLPV, pp. 47\u201356. ACM, New York (2007)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq - rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/10930755_8","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Sch\u00fcrmann","year":"2003","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D.A., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 120\u2013135. Springer, Heidelberg (2003)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"3_CR13","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7 (1994)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02444-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T13:31:52Z","timestamp":1552051912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02444-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642024436","9783642024443"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02444-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}