{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:37:44Z","timestamp":1742913464519,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_24","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"288-303","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The Role of Indirections in Lazy Natural Semantics"],"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","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"key":"24_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":"24_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), Montreal, Canada, pp. 162\u2013173, September 2000","DOI":"10.1145\/357766.351256"},{"key":"24_CR3","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)"},{"key":"24_CR4","unstructured":"Bertot, Y.: Coq in a hurry. CoRR, abs\/cs\/0603118 (2006)"},{"key":"24_CR5","unstructured":"Breitner, J.: The correctness of launchbury\u2019s natural semantics for lazy evaluation. Archive of Formal Proofs, January 2013. Formal proof development, Amended version May 2014. http:\/\/afp.sf.net\/entries\/Launchbury.shtml"},{"issue":"3","key":"24_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"46","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 46(3), 363\u2013408 (2012)","journal-title":"J. Autom. Reason."},{"issue":"5","key":"24_CR7","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","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. Indag. Math. 75(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"issue":"2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1142\/S0129626402000938","volume":"12","author":"M Hidalgo-Herrero","year":"2002","unstructured":"Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: An operational semantics for the parallel language Eden. Parallel Process. Lett. (World Scientific Publishing Company) 12(2), 211\u2013228 (2002)","journal-title":"Parallel Process. Lett. (World Scientific Publishing Company)"},{"key":"24_CR9","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"},{"issue":"6","key":"24_CR10","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796809990219","volume":"19","author":"K Nakata","year":"2009","unstructured":"Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. J. Funct. Program. 19(6), 699\u2013722 (2009)","journal-title":"J. Funct. Program."},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"24_CR12","unstructured":"S\u00e1nchez-Gil, L., Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: Call-by-need, call-by-name, and natural semantics. Technical report UU-CS-2010-020, Department of Information and Computing Sciences, Utrech University (2010)"},{"key":"24_CR13","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, pp. 65\u201380, vol. 10. Intellect (2010)","DOI":"10.2307\/j.ctv36xvmkd.8"},{"key":"24_CR14","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. Univ. Complutense de Madrid (2012). http:\/\/federwin.sip.ucm.es\/sic\/investigacion\/publicaciones\/pdfs\/SIC-1-12.pdf"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-32943-2_8","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"L S\u00e1nchez-Gil","year":"2012","unstructured":"S\u00e1nchez-Gil, L., Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: A locally nameless representation for a natural semantics for lazy evaluation. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 105\u2013119. Springer, Heidelberg (2012)"},{"key":"24_CR16","unstructured":"S\u00e1nchez-Gil, L., Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: The role of indirections in lazy natural semantics (extended version). Technical report 13\/13, Dpt. Sistemas Inform\u00e1ticos y Computaci\u00f3n. Univ. Complutense de Madrid (2013). http:\/\/federwin.sip.ucm.es\/sic\/investigacion\/publicaciones\/pdfs\/TR-13-13.pdf"},{"issue":"3","key":"24_CR17","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. J. Funct. Program. 7(3), 231\u2013264 (1997)","journal-title":"J. Funct. Program."},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science (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. 4603, pp. 35\u201350. Springer, Heidelberg (2007)"},{"issue":"2:14","key":"24_CR19","first-page":"1","volume":"8","author":"C Urban","year":"2012","unstructured":"Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in nominal Isabelle. Log. Methods Comput. Sci. 8(2:14), 1\u201335 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"24_CR20","unstructured":"van Eekelen, M., de Mol, M.: Proving lazy folklore with mixed lazy\/strict semantics. In: Barendsen, E., Capretta, V., Geuvers, H., Niqui, M. (eds.) Reflections on Type Theory, $$\\lambda $$-calculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday, pp. 87\u2013101. Radboud University Nijmegen (2007)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,9]],"date-time":"2023-08-09T15:46:06Z","timestamp":1691595966000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}