{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:41:13Z","timestamp":1748367673868},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319712369"},{"type":"electronic","value":"9783319712376"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-71237-6_21","type":"book-chapter","created":{"date-parts":[[2017,11,18]],"date-time":"2017-11-18T01:13:02Z","timestamp":1510967582000},"page":"426-447","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The Negligible and Yet Subtle Cost of Pattern Matching"],"prefix":"10.1007","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Barras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"issue":"4","key":"21_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"21_CR2","unstructured":"Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: RTA, pp. 6\u201321 (2012)"},{"key":"21_CR3","unstructured":"Accattoli, B.: COCA HOLA (2016). https:\/\/sites.google.com\/site\/beniaminoaccattoli\/coca-hola"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Accattoli, B.: The complexity of abstract machines. In: WPTE@FSCD 2016, pp. 1\u201315 (2016)","DOI":"10.4204\/EPTCS.235.1"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-52921-8_1","volume-title":"Logic, Language, Information, and Computation","author":"B Accattoli","year":"2016","unstructured":"Accattoli, B.: The useful MAM, a reasonable implementation of the strong $$\\lambda $$ \u03bb -calculus. In: V\u00e4\u00e4n\u00e4nen, J., Hirvonen, \u00c5., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 1\u201321. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-52921-8_1"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP 2014, pp. 363\u2013376. ACM (2014)","DOI":"10.1145\/2628136.2628154"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barras, B.: Environments and the complexity of abstract machines (2017). Accepted to PPDP 2017","DOI":"10.1145\/3131851.3131855"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL, pp. 659\u2013670 (2014)","DOI":"10.1145\/2535838.2535886"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Coen, C.S.: On the relative usefulness of fireballs. In: LICS 2015, pp. 141\u2013155. IEEE Computer Society (2015)","DOI":"10.1109\/LICS.2015.23"},{"issue":"1","key":"21_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-12(1:4)2016","volume":"12","author":"B Accattoli","year":"2016","unstructured":"Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Logical Methods Comput. Sci. 12(1), 1\u201346 (2016)","journal-title":"Logical Methods Comput. Sci."},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-47958-3_12","volume-title":"Programming Languages and Systems","author":"B Accattoli","year":"2016","unstructured":"Accattoli, B., Guerrieri, G.: Open call-by-value. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 206\u2013226. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_12"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-68972-2_1","volume-title":"Fundamentals of Software Engineering","author":"B Accattoli","year":"2017","unstructured":"Accattoli, B., Guerrieri, G.: Implementing open call-by-value. In: Dastani, M., Sirjani, M. (eds.) FSEN 2017. LNCS, vol. 10522, pp. 1\u201319. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68972-2_1"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-29822-6_4","volume-title":"Functional and Logic Programming","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Paolini, L.: Call-by-value solvability, revisited. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 4\u201316. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-662-44145-9_3","volume-title":"Logic, Language, Information, and Computation","author":"B Accattoli","year":"2014","unstructured":"Accattoli, B., Sacerdoti Coen, C.: On the value of variables. In: Kohlenbach, U., Barcel\u00f3, P., de Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 36\u201350. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44145-9_3"},{"issue":"3","key":"21_CR15","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"ZM Ariola","year":"1997","unstructured":"Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265\u2013301 (1997)","journal-title":"J. Funct. Program."},{"key":"21_CR16","unstructured":"Barras, B.: Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. Ph.D. thesis, Universit\u00e9 Paris 7 (1999)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Blelloch, G.E., Greiner, J.: Parallelism in sequential functional languages. In: FPCA 1995, pp. 226\u2013237. ACM (1995)","DOI":"10.1145\/224164.224210"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-22102-1_9","volume-title":"Interactive Theorem Proving","author":"A Chargu\u00e9raud","year":"2015","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 137\u2013153. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_9"},{"issue":"3","key":"21_CR19","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1093\/jigpal\/9.3.339","volume":"9","author":"H Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus - part I. Logic J. IGPL 9(3), 339\u2013375 (2001)","journal-title":"Logic J. IGPL"},{"key":"21_CR20","unstructured":"Coq Development Team: The coq proof-assistant reference manual, version 8.6 (2016). http:\/\/coq.inria.fr"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-15331-0_7","volume-title":"Foundational and Practical Aspects of Resource Analysis","author":"U Lago Dal","year":"2010","unstructured":"Dal Lago, U., Martini, S.: Derivational complexity is an invariant cost model. In: van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2009. LNCS, vol. 6324, pp. 100\u2013113. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15331-0_7"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-02930-1_14","volume-title":"Automata, Languages and Programming","author":"U Lago Dal","year":"2009","unstructured":"Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 163\u2013174. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02930-1_14"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP 2013, pp. 97\u2013108. ACM (2013)","DOI":"10.1145\/2505879.2505898"},{"key":"21_CR24","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/j.entcs.2009.03.035","volume":"237","author":"M Fern\u00e1ndez","year":"2009","unstructured":"Fern\u00e1ndez, M., Siafakas, N.: New developments in environment machines. Electr. Notes Theor. Comput. Sci. 237, 57\u201373 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235\u2013246. ACM (2002)","DOI":"10.1145\/583852.581501"},{"issue":"2","key":"21_CR26","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S0956796808007144","volume":"19","author":"CB Jay","year":"2009","unstructured":"Jay, C.B., Kesner, D.: First-class patterns. J. Funct. Program. 19(2), 191\u2013225 (2009)","journal-title":"J. Funct. Program."},{"issue":"2\u20134","key":"21_CR27","first-page":"185","volume":"17","author":"J Jeannin","year":"2012","unstructured":"Jeannin, J., Kozen, D.: Computing with capsules. J. Automata Lang. Comb. 17(2\u20134), 185\u2013204 (2012)","journal-title":"J. Automata Lang. Comb."},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-540-74915-8_20","volume-title":"Computer Science Logic","author":"D Kesner","year":"2007","unstructured":"Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238\u2013252. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_20"},{"issue":"1\u20133","key":"21_CR29","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1016\/j.tcs.2008.01.019","volume":"398","author":"JW Klop","year":"2008","unstructured":"Klop, J.W., van Oostrom, V., de Vrijer, R.C.: Lambda calculus with patterns. Theor. Comput. Sci. 398(1\u20133), 16\u201331 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: POPL 1993, pp. 144\u2013154. ACM Press (1993)","DOI":"10.1145\/158511.158618"},{"issue":"3","key":"21_CR31","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1017\/S0956796898003037","volume":"8","author":"J Maraist","year":"1998","unstructured":"Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275\u2013317 (1998)","journal-title":"J. Funct. Program."},{"issue":"3","key":"21_CR32","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/j.entcs.2006.07.035","volume":"175","author":"R Milner","year":"2007","unstructured":"Milner, R.: Local bigraphs and confluence: two conjectures. Electr. Notes Theor. Comput. Sci. 175(3), 65\u201373 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"21_CR33","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-36377-7_4","volume-title":"The Essence of Computation","author":"D Sands","year":"2002","unstructured":"Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 60\u201382. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36377-7_4"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Sergey, I., Vytiniotis, D., Peyton Jones, S.L.: Modular, higher-order cardinality analysis in theory and practice. In: POPL 2014, pp. 335\u2013348 (2014)","DOI":"10.1145\/2535838.2535861"},{"issue":"3","key":"21_CR36","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1017\/S0956796897002712","volume":"7","author":"P Sestoft","year":"1997","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231\u2013264 (1997)","journal-title":"J. Funct. Program."},{"key":"21_CR37","unstructured":"Wadsworth, C.P.: Semantics and pragmatics of the lambda-calculus. Ph.D. thesis, Oxford (1971). Chapter 4"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Walker, D.: Substructural type systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, pp. 3\u201343. The MIT Press (2004)","DOI":"10.7551\/mitpress\/1104.003.0003"},{"issue":"1","key":"21_CR39","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-71237-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T19:28:52Z","timestamp":1719602932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}