{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:07Z","timestamp":1767928327212,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T00:00:00Z","timestamp":1503964800000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,8,29]]},"abstract":"<jats:p>We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to<jats:italic>\u03b2<\/jats:italic>-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a<jats:italic>\u03b2<\/jats:italic>-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.<\/jats:p>","DOI":"10.1145\/3110264","type":"journal-article","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T18:19:41Z","timestamp":1504030781000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Foundations of strong call by need"],"prefix":"10.1145","volume":"1","author":[{"given":"Thibaut","family":"Balabonski","sequence":"first","affiliation":[{"name":"LRI, France \/ University of Paris-Sud, France \/ CNRS, France \/ University of Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo","family":"Barenbaum","sequence":"additional","affiliation":[{"name":"University of Buenos Aires, Argentina \/ IRIF, France \/ CNRS, France \/ University of Paris Diderot, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eduardo","family":"Bonelli","sequence":"additional","affiliation":[{"name":"CONICET, Argentina \/ Universidad Nacional de Quilmes, Argentina \/ Stevens Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[{"name":"IRIF, France \/ CNRS, France \/ University of Paris Diderot, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912)","volume":"15","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli . 2012 . An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912) , May 28 - June 2, 2012, Nagoya, Japan (LIPIcs), Ashish Tiwari (Ed.), Vol. 15 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6\u201321. Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912), May 28 - June 2, 2012, Nagoya, Japan (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6\u201321."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_13"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_12"},{"key":"e_1_2_1_5_1","volume-title":"24th International Workshop (CSL\u201910), 19th Annual Conference of the EACSL","volume":"6247","author":"Accattoli Beniamino","year":"2010","unstructured":"Beniamino Accattoli and Delia Kesner . 2010 . The Structural lambda-Calculus. In Computer Science Logic , 24th International Workshop (CSL\u201910), 19th Annual Conference of the EACSL , Brno, Czech Republic , August 23-27, 2010. (LNCS), Anuj Dawar and Helmut Veith (Eds.), Vol. 6247 . Springer Verlag, 381\u2013395. Beniamino Accattoli and Delia Kesner. 2010. The Structural lambda-Calculus. In Computer Science Logic, 24th International Workshop (CSL\u201910), 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. (LNCS), Anuj Dawar and Helmut Veith (Eds.), Vol. 6247. Springer Verlag, 381\u2013395."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_2_1_9_1","volume-title":"The Optimal Implementation of Functional Programming Languages","author":"Asperti Andrea","unstructured":"Andrea Asperti and Stefano Guerrini . 1998. The Optimal Implementation of Functional Programming Languages . Cambridge Tracts in Theoretical Computer Science, Vol. 45 . Cambridge University Press . Andrea Asperti and Stefano Guerrini. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, Vol. 45. Cambridge University Press."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500606"},{"key":"e_1_2_1_12_1","volume-title":"Personal Communication. (February","author":"Barras B.","year":"2017","unstructured":"B. Barras . 2017. Personal Communication. (February 2017 ). B. Barras. 2017. Personal Communication. (February 2017)."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:3)2013"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"e_1_2_1_16_1","volume-title":"Non-Idempotent Intersection Types for the Lambda-Calculus. Logic Journal of the IGPL","author":"Bucciarelli Antonio","year":"2017","unstructured":"Antonio Bucciarelli , Delia Kesner , and Daniel Ventura . 2017. Non-Idempotent Intersection Types for the Lambda-Calculus. Logic Journal of the IGPL ( 2017 ). To appear. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-Idempotent Intersection Types for the Lambda-Calculus. Logic Journal of the IGPL (2017). To appear."},{"key":"e_1_2_1_17_1","volume-title":"Programming Languages and Systems - 21st European Symposium on Programming (ESOP\u201912), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS","author":"Chang Stephen","year":"2012","unstructured":"Stephen Chang and Matthias Felleisen . 2012. The Call-by-Need Lambda Calculus , Revisited. In Programming Languages and Systems - 21st European Symposium on Programming (ESOP\u201912), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 , Tallinn, Estonia, March 24 - April 1, 2012. (LNCS), Helmut Seidl (Ed.), Vol. 7211 . Springer Verlag , 128\u2013147. Stephen Chang and Matthias Felleisen. 2012. The Call-by-Need Lambda Calculus, Revisited. In Programming Languages and Systems - 21st European Symposium on Programming (ESOP\u201912), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. (LNCS), Helmut Seidl (Ed.), Vol. 7211. Springer Verlag, 128\u2013147."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91681"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9015-z"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and Ian Zerny. 2013. A synthetic operational account of call-by-need evaluation See [ Pe\u00f1a and Schrijvers 2013 ] 97\u2013108. Olivier Danvy and Ian Zerny. 2013. A synthetic operational account of call-by-need evaluation See [ Pe\u00f1a and Schrijvers 2013 ] 97\u2013108.","DOI":"10.1145\/2505879.2505898"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.121.4"},{"key":"e_1_2_1_25_1","volume-title":"Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251","author":"de Carvalho Daniel","year":"2009","unstructured":"Daniel de Carvalho . 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251 ( 2009 ), 1\u201336. Daniel de Carvalho. 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs\/0905.4251 (2009), 1\u201336."},{"key":"e_1_2_1_26_1","volume-title":"Logical Approaches to Computational Barriers, Second Conference on Computability in Europe (CiE\u201906)","author":"Ehrhard Thomas","year":"2006","unstructured":"Thomas Ehrhard and Laurent Regnier . 2006. B\u00f6hm Trees , Krivine\u2019s Machine and the Taylor Expansion of Lambda-Terms . In Logical Approaches to Computational Barriers, Second Conference on Computability in Europe (CiE\u201906) , Swansea, UK , June 30-July 5, 2006 . (LNCS), Arnold Beckmann, Ulrich Berger, Benedikt L\u00f6we, and John V. Tucker (Eds.), Vol. 3988 . Springer Verlag , 186\u2013197. Thomas Ehrhard and Laurent Regnier. 2006. B\u00f6hm Trees, Krivine\u2019s Machine and the Taylor Expansion of Lambda-Terms. In Logical Approaches to Computational Barriers, Second Conference on Computability in Europe (CiE\u201906), Swansea, UK, June 30-July 5, 2006. (LNCS), Arnold Beckmann, Ulrich Berger, Benedikt L\u00f6we, and John V. Tucker (Eds.), Vol. 3988. Springer Verlag, 186\u2013197."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_115"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/800168.811543"},{"key":"e_1_2_1_30_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones Simon L.","unstructured":"Simon L. Peyton Jones . 1987. The Implementation of Functional Programming Languages . Prentice-Hall . Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:1)2009"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_25"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44602-7_23"},{"key":"e_1_2_1_34_1","volume-title":"Theoretical Aspects of Computing (ICTAC) (LNCS), Martin Leucker, Camilo Rueda, and Frank D","author":"Kesner Delia","unstructured":"Delia Kesner and Daniel Ventura . 2015. A resource aware computational interpretation for Herberlin\u2019s syntax . In Theoretical Aspects of Computing (ICTAC) (LNCS), Martin Leucker, Camilo Rueda, and Frank D . Valencia (Eds.), Vol. 9399 . Springer Verlag , 1\u201316. Delia Kesner and Daniel Ventura. 2015. A resource aware computational interpretation for Herberlin\u2019s syntax. In Theoretical Aspects of Computing (ICTAC) (LNCS), Martin Leucker, Camilo Rueda, and Frank D. Valencia (Eds.), Vol. 9399. Springer Verlag, 1\u201316."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.032"},{"key":"e_1_2_1_37_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Ellis Horwood. Jean-Louis Krivine. 1993. Lambda-calculus types and models. Ellis Horwood."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96711"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_40_1","volume-title":"To Haskell Brooks Curry: Essays in Combinatory Logic, Lambda Calculus and formalism, Roger Hindley and Jonathan P","author":"L\u00e9vy Jean-Jacques","unstructured":"Jean-Jacques L\u00e9vy . 1980. Optimal Reductions in the lambda-calculus . In To Haskell Brooks Curry: Essays in Combinatory Logic, Lambda Calculus and formalism, Roger Hindley and Jonathan P . Seldin (Eds.). Academic Press , 159\u2013191. Jean-Jacques L\u00e9vy. 1980. Optimal Reductions in the lambda-calculus. In To Haskell Brooks Curry: Essays in Combinatory Logic, Lambda Calculus and formalism, Roger Hindley and Jonathan P. Seldin (Eds.). Academic Press, 159\u2013191."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003037"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_45_1","unstructured":"The Coq Development Team. 2017. The Coq Proof Assistant (v8.6). (2017). https:\/\/github.com\/coq\/coq . The Coq Development Team. 2017. The Coq Proof Assistant (v8.6). (2017). https:\/\/github.com\/coq\/coq ."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110264","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3110264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3110264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,29]]},"references-count":44,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2017,8,29]]}},"alternative-id":["10.1145\/3110264"],"URL":"https:\/\/doi.org\/10.1145\/3110264","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,29]]},"assertion":[{"value":"2017-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}