{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:47Z","timestamp":1750306787330,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T00:00:00Z","timestamp":1379289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,9,16]]},"DOI":"10.1145\/2505879.2505898","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"97-108","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["A synthetic operational account of call-by-need evaluation"],"prefix":"10.1145","author":[{"given":"Olivier","family":"Danvy","sequence":"first","affiliation":[{"name":"Aarhus University"}]},{"given":"Ian","family":"Zerny","sequence":"additional","affiliation":[{"name":"Aarhus University"}]}],"member":"320","published-online":{"date-parts":[[2013,9,16]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.02.012"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_6"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-642-21691-6_6","volume-title":"Typed Lambda Calculi and Applications","author":"Ariola Z. M.","year":"2011","unstructured":"Z. M. Ariola , H. Herbelin , and A. Saurin . Classical call-by-need and duality . In L. Ong, editor, Typed Lambda Calculi and Applications , International Conference, TLCA 2011 , number 6690 in Lecture Notes in Computer Science , pages 27 -- 44 , Novi Sad, Serbia, June 2011. Springer . Z. M. Ariola, H. Herbelin, and A. Saurin. Classical call-by-need and duality. In L. Ong, editor, Typed Lambda Calculi and Applications, International Conference, TLCA 2011, number 6690 in Lecture Notes in Computer Science, pages 27--44, Novi Sad, Serbia, June 2011. Springer."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103713"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(96)00040-8"},{"key":"e_1_3_2_1_10_1","first-page":"141","volume-title":"Parallel Languages, number 259 in Lecture Notes in Computer Science","author":"Barendregt H. P.","year":"1987","unstructured":"H. P. Barendregt , M. C. J. D. van Eekelen , J. R. W. Glauert , R. Kennaway , M. J. Plasmeijer , and M. R. Sleep . Term graph rewriting . In J. de Bakker, A. J. Nijman, and P. C. Treleaven, editors, PARLE, Parallel Architectures and Languages Europe, Volume II : Parallel Languages, number 259 in Lecture Notes in Computer Science , pages 141 -- 158 , Eindhoven, The Netherlands, June 1987 . Springer-Verlag . H. P. Barendregt, M. C. J. D. van Eekelen, J. R. W. Glauert, R. Kennaway, M. J. Plasmeijer, and M. R. Sleep. Term graph rewriting. In J. de Bakker, A. J. Nijman, and P. C. Treleaven, editors, PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages, number 259 in Lecture Notes in Computer Science, pages 141--158, Eindhoven, The Netherlands, June 1987. Springer-Verlag."},{"key":"e_1_3_2_1_11_1","volume-title":"Artificial Intelligence Laboratory","author":"Beeler M.","year":"1972","unstructured":"M. Beeler , R. W. Gosper , and R. Schroeppel . HAKMEM. AI Memo 239 , Artificial Intelligence Laboratory , Massachusetts Institute of Technology , Cambridge, Massachusetts , Feb. 1972 . http:\/\/home.pipeline.com\/~hbaker1\/hakmem\/. M. Beeler, R. W. Gosper, and R. Schroeppel. HAKMEM. AI Memo 239, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, Feb. 1972. http:\/\/home.pipeline.com\/~hbaker1\/hakmem\/."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297664"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.028"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_7"},{"key":"e_1_3_2_1_15_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-23456-9","volume-title":"Trends in Functional Programming","author":"Chang S.","year":"2011","unstructured":"S. Chang , D. V. Horn , and M. Felleisen . Evaluating call by need on the control stack . In R. Page, Z. Horv\u00e1th, and V. Zs\u00f3k, editors, Trends in Functional Programming , Volume 11 , number 6546 in Lecture Notes in Computer Science , pages 1 -- 15 , Norman, Oklahoma, May 2011 . Springer . S. Chang, D. V. Horn, and M. Felleisen. Evaluating call by need on the control stack. In R. Page, Z. Horv\u00e1th, and V. Zs\u00f3k, editors, Trends in Functional Programming, Volume 11, number 6546 in Lecture Notes in Computer Science, pages 1--15, Norman, Oklahoma, May 2011. Springer."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9015-z"},{"key":"e_1_3_2_1_17_1","first-page":"66","volume-title":"Advanced Functional Programming, Sixth International School, number 5382 in Lecture Notes in Computer Science","author":"Danvy O.","year":"2008","unstructured":"O. Danvy . From reduction-based to reduction-free normalization . In P. Koopman, R. Plasmeijer, and D. Swierstra, editors, Advanced Functional Programming, Sixth International School, number 5382 in Lecture Notes in Computer Science , pages 66 -- 164 , Nijmegen, The Netherlands , May 2008 . Springer . O. Danvy. From reduction-based to reduction-free normalization. In P. Koopman, R. Plasmeijer, and D. Swierstra, editors, Advanced Functional Programming, Sixth International School, number 5382 in Lecture Notes in Computer Science, pages 66--164, Nijmegen, The Netherlands, May 2008. Springer."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.10.010"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.023"},{"key":"e_1_3_2_1_20_1","volume-title":"Department of Computer Science","author":"Danvy O.","year":"2004","unstructured":"O. Danvy and L. R. Nielsen . Refocusing in reduction semantics. Research Report BRICS RS-04-26 , Department of Computer Science , Aarhus University, Aarhus , Denmark, Nov . 2004 . A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4. O. Danvy and L. R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, Aarhus, Denmark, Nov. 2004. A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4."},{"key":"e_1_3_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"120","volume-title":"Logic Based Program Synthesis and Transformation, 20th International Symposium, LOPSTR","author":"Danvy O.","year":"2010","unstructured":"O. Danvy and I. Zerny . Three syntactic theories for combinatory graph reduction . In M. Alpuente, editor, Logic Based Program Synthesis and Transformation, 20th International Symposium, LOPSTR 2010 , revised selected papers, number 6564 in Lecture Notes in Computer Science , pages 120 , Hagenberg, Austria, July 2010. Springer . Invited talk. Extended version to appear in ACM Transactions on Computational Logic. O. Danvy and I. Zerny. Three syntactic theories for combinatory graph reduction. In M. Alpuente, editor, Logic Based Program Synthesis and Transformation, 20th International Symposium, LOPSTR 2010, revised selected papers, number 6564 in Lecture Notes in Computer Science, pages 120, Hagenberg, Austria, July 2010. Springer. Invited talk. Extended version to appear in ACM Transactions on Computational Logic."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-739X(99)00088-6"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/276393.276397"},{"key":"e_1_3_2_1_24_1","first-page":"34","volume-title":"Functional Programming Languages and Computer Architecture, number 274 in Lecture Notes in Computer Science","author":"Fairbairn J.","year":"1987","unstructured":"J. Fairbairn and S. Wray . TIM: a simple, lazy abstract machine to execute supercombinators . In G. Kahn, editor, Functional Programming Languages and Computer Architecture, number 274 in Lecture Notes in Computer Science , pages 34 -- 45 , Portland, Oregon, Sept . 1987 . Springer-Verlag . J. Fairbairn and S. Wray. TIM: a simple, lazy abstract machine to execute supercombinators. In G. Kahn, editor, Functional Programming Languages and Computer Architecture, number 274 in Lecture Notes in Computer Science, pages 34--45, Portland, Oregon, Sept. 1987. Springer-Verlag."},{"key":"e_1_3_2_1_25_1","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen M.","year":"2009","unstructured":"M. Felleisen , R. B. Findler , and M. Flatt . Semantics Engineering with PLT Redex . The MIT Press , 2009 . M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. The MIT Press, 2009."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9014-0"},{"key":"e_1_3_2_1_27_1","first-page":"257","volume-title":"Third International Colloquium on Automata, Languages, and Programming","author":"Friedman D. P.","year":"1976","unstructured":"D. P. Friedman and D. S. Wise . CONS should not evaluate its arguments . In S. Michaelson and R. Milner, editors, Third International Colloquium on Automata, Languages, and Programming , pages 257 -- 284 . Edinburgh University Press, Edinburgh , Scotland, July 1976 . D. P. Friedman and D. S. Wise. CONS should not evaluate its arguments. In S. Michaelson and R. Milner, editors, Third International Colloquium on Automata, Languages, and Programming, pages 257--284. Edinburgh University Press, Edinburgh, Scotland, July 1976."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480903"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002986"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/800168.811543"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_2_1_33_1","volume-title":"Universit\u00e9 de Paris VII","author":"L\u00e9vy J.-J.","year":"1978","unstructured":"J.-J. L\u00e9vy . R\u00e9ductions correctes et optimales dans le lambda-calcul. Th\u00e8se d'\u00e9tat , Universit\u00e9 de Paris VII , Paris, France , 1978 . J.-J. L\u00e9vy. R\u00e9ductions correctes et optimales dans le lambda-calcul. Th\u00e8se d'\u00e9tat, Universit\u00e9 de Paris VII, Paris, France, 1978."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003037"},{"key":"e_1_3_2_1_35_1","volume-title":"Prentice Hall International","author":"Milner R.","year":"1989","unstructured":"R. Milner . Communication and Concurrency . Prentice Hall International , 1989 . R. Milner. Communication and Concurrency. Prentice Hall International, 1989."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990219"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190241"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863528"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010075320153"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_3_2_1_44_1","series-title":"Lecture Notes in Computer Science","first-page":"72","volume-title":"Implementation and Application of Functional Languages, -- 22nd International Symposium, IFL","author":"Sieczkowski F.","year":"2010","unstructured":"F. Sieczkowski , M. Biernacka , and D. Biernacki . Automating derivations of abstract machines from reduction semantics: A generic formalization of refocusing in Coq . In J. Hage and M. T. Moraz\u00e1n, editors, Implementation and Application of Functional Languages, -- 22nd International Symposium, IFL 2010 , number 6647 in Lecture Notes in Computer Science , pages 72 -- 88 , Alphen aan den Rijn, The Netherlands, Sept. 2010. Springer . Revised Selected Papers. F. Sieczkowski, M. Biernacka, and D. Biernacki. Automating derivations of abstract machines from reduction semantics: A generic formalization of refocusing in Coq. In J. Hage and M. T. Moraz\u00e1n, editors, Implementation and Application of Functional Languages, -- 22nd International Symposium, IFL 2010, number 6647 in Lecture Notes in Computer Science, pages 72--88, Alphen aan den Rijn, The Netherlands, Sept. 2010. Springer. Revised Selected Papers."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"e_1_3_2_1_46_1","volume-title":"Oxford University","author":"Wadsworth C. P.","year":"1971","unstructured":"C. P. Wadsworth . Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Computing Laboratory , Oxford University , Oxford, UK , 1971 . C. P. Wadsworth. Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Computing Laboratory, Oxford University, Oxford, UK, 1971."}],"event":{"name":"PPDP '13: 15th International Symposium on Principles and Practice of Declarative Programming","sponsor":["Universidad Complutense de Madrid","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Madrid Spain","acronym":"PPDP '13"},"container-title":["Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505898","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2505879.2505898","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:17Z","timestamp":1750232057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2505879.2505898"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,16]]},"references-count":45,"alternative-id":["10.1145\/2505879.2505898","10.1145\/2505879"],"URL":"https:\/\/doi.org\/10.1145\/2505879.2505898","relation":{},"subject":[],"published":{"date-parts":[[2013,9,16]]},"assertion":[{"value":"2013-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}