{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T22:10:02Z","timestamp":1748815802353,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662494974"},{"type":"electronic","value":"9783662494981"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_24","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"616-643","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Classical By-Need"],"prefix":"10.1007","author":[{"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"first","affiliation":[]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"24_CR1","doi-asserted-by":"publisher","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":"24_CR2","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, Chakravarty (eds.) ICFP 2014, pp. 363\u2013376. ACM (2014)","DOI":"10.1145\/2692915.2628154"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: POPL 2014, San Diego, CA, USA, pp. 659\u2013670 (2014)","DOI":"10.1145\/2535838.2535886"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-15205-4_30","volume-title":"Computer Science Logic","author":"B Accattoli","year":"2010","unstructured":"Accattoli, B., Kesner, D.: The structural $$\\lambda $$ \u03bb -calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381\u2013395. Springer, Heidelberg (2010)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-28717-6_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Accattoli","year":"2012","unstructured":"Accattoli, B., Kesner, D.: The permutative $$\\lambda $$ \u03bb -calculus. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 23\u201336. Springer, Heidelberg (2012)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Lago, U.D.: Beta reduction is invariant, indeed. In: CSL-LICS 2014, Vienna, Austria, July 2014","DOI":"10.1145\/2603088.2603105"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-29822-6_6","volume-title":"Functional and Logic Programming","author":"ZM Ariola","year":"2012","unstructured":"Ariola, Z.M., Downen, P., Herbelin, H., Nakata, K., Saurin, A.: Classical call-by-need sequent calculi: the unity of semantic artifacts. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 32\u201346. Springer, Heidelberg (2012)"},{"issue":"3","key":"24_CR8","doi-asserted-by":"publisher","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":"24_CR9","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. In: POPL 1995, pp. 233\u2013246. ACM Press (1995)","DOI":"10.1145\/199448.199507"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-642-21691-6_6","volume-title":"Typed Lambda Calculi and Applications","author":"ZM Ariola","year":"2011","unstructured":"Ariola, Z.M., Herbelin, H., Saurin, A.: Classical call-by-need and duality. In: Ong, L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol. 6690, pp. 27\u201344. Springer, Heidelberg (2011)"},{"key":"24_CR11","volume-title":"The Lambda Calculus, its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics","author":"H Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus, its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam (1984)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-28869-2_7","volume-title":"Programming Languages and Systems","author":"S Chang","year":"2012","unstructured":"Chang, S., Felleisen, M.: The call-by-need lambda calculus, revisited. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 128\u2013147. Springer, Heidelberg (2012)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Odersky, M., Wadler, P. (eds.) ICFP 2000, pp. 233\u2013243. ACM Press (2000)","DOI":"10.1145\/357766.351262"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Danos, V., Herbelin, H., Regnier, L.: Game semantics & abstract machines. In: LICS 1996, pp. 394\u2013405. IEEE Press (1996)","DOI":"10.1109\/LICS.1996.561456"},{"key":"24_CR15","unstructured":"Danos, V., Regnier, L.: Head linear reduction (2004) (unpublished)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-12251-4_18","volume-title":"Functional and Logic Programming","author":"O Danvy","year":"2010","unstructured":"Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized interpreters for call-by-need evaluation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 240\u2013256. Springer, Heidelberg (2010)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Une extension de l\u2019interprtation de Gdel l\u2019analyse, et sonapplication a l\u2019\u00e9limination des coupures dans l\u2019analyse et la thorie destypes. In: Fenstad (ed.) Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63\u201392. Elsevier (1971)","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"24_CR19","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"M Hyland","year":"2000","unstructured":"Hyland, M., Ong, L.: On full abstraction for PCF. Inf. Comput. 163(2), 285\u2013408 (2000)","journal-title":"Inf. Comput."},{"issue":"3","key":"24_CR20","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"J-L Krivine","year":"2007","unstructured":"Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher-Order Symb. Comput. 20(3), 199\u2013207 (2007)","journal-title":"Higher-Order Symb. Comput."},{"key":"24_CR21","unstructured":"Laurent, O.: A study of polarization in logic. Ph.D. Thesis, Universit\u00e9 de la M\u00e9diterran\u00e9e - Aix-Marseille II, March 2002"},{"issue":"3","key":"24_CR22","doi-asserted-by":"publisher","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."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Miquel, A.: Forcing as a program transformation. In: LICS, pp. 197\u2013206. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.47"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"24_CR25","unstructured":"Regnier, L.: Lambda-calcul et r\u00e9seaux. Ph.D. Thesis, Univ. Paris VII (1992)"},{"key":"24_CR26","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"126","author":"L Regnier","year":"1994","unstructured":"Regnier, L.: Une \u00e9quivalence sur les $$\\lambda $$ \u03bb -termes. Theoret. Comput. Sci. 126, 281\u2013292 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Programming Symposium","author":"JC Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408\u2013423. Springer, Heidelberg (1974)"},{"issue":"3\u20134","key":"24_CR28","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF01019459","volume":"6","author":"JC Reynolds","year":"1993","unstructured":"Reynolds, J.C.: The discoveries of continuations. Lisp Symb. Comput. 6(3\u20134), 233\u2013248 (1993)","journal-title":"Lisp Symb. Comput."},{"issue":"6","key":"24_CR29","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1017\/S0956796898003141","volume":"8","author":"T Streicher","year":"1998","unstructured":"Streicher, T., Reus, B.: Classical logic, continuation semantics and abstract machines. J. Funct. Program. 8(6), 543\u2013572 (1998)","journal-title":"J. Funct. Program."},{"key":"24_CR30","unstructured":"Wadsworth, C.P.: Semantics and pragmatics of the lambda-calculus. Ph.D. Thesis, Programming Research Group, Oxford University (1971)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:35:19Z","timestamp":1748813719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}