{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:53Z","timestamp":1774837853956,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_29","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"419-434","source":"Crossref","is-referenced-by-count":29,"title":["Equations: A Dependent Pattern-Matching Compiler"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","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":"29_CR2","unstructured":"Coquand, T.: Pattern Matching with Dependent Types. In: Proceedings of the Workshop on Logical Frameworks (1992)"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Compiling Pattern Matching. In: FPCA, pp. 368\u2013381 (1985)","DOI":"10.1007\/3-540-15975-4_48"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02444-3_3","volume-title":"Types for Proofs and Programs","author":"B. Barras","year":"2009","unstructured":"Barras, B., Corbineau, P., Gr\u00e9goire, B., Herbelin, H., Sacchini, J.L.: A New Elimination Rule for the Calculus of Inductive Constructions. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 32\u201348. Springer, Heidelberg (2009)"},{"key":"29_CR5","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden (2007)"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","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, pp. 197\u2013216. Springer, Heidelberg (2002)"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"McBride, C., Goguen, H., McKinna, J.: A Few Constructions on Constructors. Types for Proofs and Programs, 186\u2013200 (2004)","DOI":"10.1007\/11617990_12"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"29_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory","author":"T. Streicher","year":"1991","unstructured":"Streicher, T.: Semantics of Type Theory. Springer, Heidelberg (1991)"},{"key":"29_CR10","unstructured":"Cornes, C.: Conception d\u2019un langage de haut niveau de repr\u00e9sentation de preuves: R\u00e9currence par filtrage de motifs, Unification en pr\u00e9sesence de types inductifs primitifs, Synth\u00e9se de lemmes d\u2019inversion. PhD thesis, Universit\u00e9 Paris 7 (1997)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/BFb0097795","volume-title":"Types for Proofs and Programs","author":"C. McBride","year":"1998","unstructured":"McBride, C.: Inverting Inductively Defined Relations in LEGO. In: Gim\u00e9nez, E., Paulin-Mohring, C. (eds.) TYPES 1996. LNCS, vol.\u00a01512, pp. 236\u2013253. Springer, Heidelberg (1998)"},{"key":"29_CR12","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, 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. Functional and Logic Programming, 114\u2013129 (2006)","DOI":"10.1007\/11737414_9"},{"key":"29_CR14","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1017\/S0960129505004822","volume":"15","author":"A. Bove","year":"2005","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory. Mathematical Structures in Computer Science\u00a015, 671\u2013708 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"29_CR15","unstructured":"Sozeau, M.: Un environnement pour la programmation avec types d\u00e9pendants. PhD thesis, Universit\u00e9 Paris 11, Orsay, France (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:02Z","timestamp":1606186022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}