{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T09:29:05Z","timestamp":1725701345244},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329425"},{"type":"electronic","value":"9783642329432"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32943-2_8","type":"book-chapter","created":{"date-parts":[[2012,8,28]],"date-time":"2012-08-28T04:59:35Z","timestamp":1346129975000},"page":"105-119","source":"Crossref","is-referenced-by-count":3,"title":["A Locally Nameless Representation for a Natural Semantics for Lazy Evaluation"],"prefix":"10.1007","author":[{"given":"Lidia","family":"S\u00e1nchez-Gil","sequence":"first","affiliation":[]},{"given":"Mercedes","family":"Hidalgo-Herrero","sequence":"additional","affiliation":[]},{"given":"Yolanda","family":"Ortega-Mall\u00e9n","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: ACM Symposium on Principles of Programming Languages, POPL 2008, pp. 3\u201315. ACM Press (2008)","DOI":"10.1145\/1328897.1328443"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Baker-Finch, C., King, D., Trinder, P.W.: An operational semantics for parallel lazy evaluation. In: ACM-SIGPLAN International Conference on Functional Programming (ICFP 2000), pp. 162\u2013173. ACM Press (2000)","DOI":"10.1145\/357766.351256"},{"key":"8_CR3","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol.\u00a0103. North-Holland (1984)"},{"key":"8_CR4","unstructured":"Bertot, Y.: Coq in a hurry. CoRR, abs\/cs\/0603118 (2006)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. Journal of Automated Reasoning, 1\u201346 (2011)","DOI":"10.1007\/s10817-011-9225-2"},{"issue":"5","key":"8_CR6","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae\u00a075(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: ACM Symposium on Principles of Programming Languages, POPL 1993, pp. 144\u2013154. ACM Press (1993)","DOI":"10.1145\/158511.158618"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. CoRR, abs\/0907.4640 (2009)","DOI":"10.1017\/S0956796809990219"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186(2), 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez-Gil, L., Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: An Operational Semantics for Distributed Lazy Evaluation. In: Trends in Functional Programming, vol.\u00a010, pp. 65\u201380. Intellect (2010)","DOI":"10.2307\/j.ctv36xvmkd.8"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez-Gil, L., Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: A locally nameless representation for a natural semantics for lazy evaluation. Technical Report 01\/12, Dpt. Sistemas Inform\u00e1ticos y Computaci\u00f3n. Universidad Complutense de Madrid (2012), http:\/\/maude.sip.ucm.es\/eden-semantics\/","DOI":"10.1007\/978-3-642-32943-2_8"},{"issue":"3","key":"8_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1017\/S0956796897002712","volume":"7","author":"P. Sestoft","year":"1997","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. Journal of Functional Programming\u00a07(3), 231\u2013264 (1997)","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"8_CR14","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automatic Reasoning\u00a040(4), 327\u2013356 (2008)","journal-title":"Journal of Automatic Reasoning"},{"key":"8_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-73595-3_4","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Urban","year":"2007","unstructured":"Urban, C., Berghofer, S., Norrish, M.: Barendregt\u2019s Variable Convention in Rule Inductions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 35\u201350. Springer, Heidelberg (2007)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-19718-5_25","volume-title":"Programming Languages and Systems","author":"C. Urban","year":"2011","unstructured":"Urban, C., Kaliszyk, C.: General Bindings and Alpha-Equivalence in Nominal Isabelle. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 480\u2013500. Springer, Heidelberg (2011)"},{"key":"8_CR17","unstructured":"van Eekelen, M., de Mol, M.: Reflections on Type Theory, \u03bb-calculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday, chapter Proving Lazy Folklore with Mixed Lazy\/Strict Semantics, pp. 87\u2013101. Radboud University Nijmegen (2007)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32943-2_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,25]],"date-time":"2023-06-25T13:00:11Z","timestamp":1687698011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32943-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329425","9783642329432"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32943-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}