{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T20:24:18Z","timestamp":1794515058581,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496299","type":"print"},{"value":"9783662496305","type":"electronic"}],"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-49630-5_25","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T05:04:32Z","timestamp":1458536672000},"page":"424-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Reasoning About Call-by-need by Means of Types"],"prefix":"10.1007","author":[{"given":"Delia","family":"Kesner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP. ACM Press (2014)","DOI":"10.1145\/2628136.2628154"},{"issue":"3","key":"25_CR2","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":"25_CR3","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. In: POPL, pp. 233\u2013246. ACM Press (1995)","DOI":"10.1145\/199448.199507"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Bull. Symbolic Logic 48, 931\u2013940 (1983)","journal-title":"Bull. Symbolic Logic"},{"issue":"4:3","key":"25_CR5","first-page":"1","volume":"9","author":"A Bernadet","year":"2013","unstructured":"Bernadet, A., Lengrand, S.: Non-idempotent intersection types and strong normalisation. Logical Methods Comput. Sci. 9(4:3), 1\u201346 (2013)","journal-title":"Logical Methods Comput. Sci."},{"issue":"4","key":"25_CR6","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1017\/S0960129599002893","volume":"9","author":"G Boudol","year":"1999","unstructured":"Boudol, G., Curien, P.-L., Lavatelli, C.: A semantics for lambda calculi with resources. Math. Struct. Comput. Sci. 9(4), 437\u2013482 (1999)","journal-title":"Math. Struct. Comput. Sci."},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-662-44602-7_26","volume-title":"Theoretical Computer Science","author":"A Bucciarelli","year":"2014","unstructured":"Bucciarelli, A., Kesner, D., Ronchi Della Rocca, S.: The inhabitation problem for non-idempotent intersection types. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 341\u2013354. Springer, Heidelberg (2014)"},{"key":"25_CR8","series-title":"APIC Series","first-page":"19","volume-title":"Logic and Computer Science","author":"F Cardone","year":"1990","unstructured":"Cardone, F., Coppo, M.: Two extension of Curry\u2019s type inference system. In: Odifreddi, P. (ed.) Logic and Computer Science. APIC Series, vol. 31, pp. 19\u201375. Academic Press, New York (1990)"},{"key":"25_CR9","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.) ESOP 2012. LNCS, vol. 7211, pp. 128\u2013147. Springer, Heidelberg (2012)"},{"issue":"2\u20136","key":"25_CR10","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1002\/malq.19810270205","volume":"27","author":"M Coppo","year":"1981","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Math. Logic Q. 27(2\u20136), 45\u201358 (1981)","journal-title":"Math. Logic Q."},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF02011875","volume":"19","author":"M Coppo","year":"1978","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: A new type-assignment for lambda terms. Archiv f\u00fcr Math. Logik Grundlagenforschung 19, 139\u2013156 (1978)","journal-title":"Archiv f\u00fcr Math. Logik Grundlagenforschung"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \n                      \n                        \n                      \n                      $$\\lambda $$\n                      \n                        \n                          \u03bb\n                        \n                      \n                    -calculus. Notre Dame J. Formal Logic 21, 685\u2013693 (1980)","journal-title":"Notre Dame J. Formal Logic"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Danvy, O., Zerny, I.: A synthetic operational account of call-by-need evaluation. In: PPDP, pp. 97\u2013108. ACM Press (2013)","DOI":"10.1145\/2505879.2505898"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"De Benedetti, E., Ronchi Della Rocca, S.: Bounding normalization time through intersection types. In: ITRS 2012, EPTCS, pp. 48\u201357 (2013)","DOI":"10.4204\/EPTCS.121.4"},{"key":"25_CR15","unstructured":"de Carvalho, D.: S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II (2007)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/3-540-57887-0_115","volume-title":"Theoretical Aspects of Computer Software","author":"P Gardner","year":"1994","unstructured":"Gardner, P.: Discovering needed reductions using type theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 555\u2013574. Springer, Heidelberg (1994)"},{"key":"25_CR17","unstructured":"Kesner, D., Ventura, D.: Quantitative types for intuitionistic calculi. Technical report (2014). \n                      https:\/\/hal.archives-ouvertes.fr\/hal-00980868"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/978-3-662-44602-7_23","volume-title":"Theoretical Computer Science","author":"D Kesner","year":"2014","unstructured":"Kesner, D., Ventura, D.: Quantitative types for the linear substitution calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 296\u2013310. Springer, Heidelberg (2014)"},{"key":"25_CR19","unstructured":"Kfoury, A.J.: A linearization of the lambda-calculus and consequences. Technical report, Boston Universsity (1996)"},{"issue":"3","key":"25_CR20","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1093\/logcom\/10.3.411","volume":"10","author":"AJ Kfoury","year":"2000","unstructured":"Kfoury, A.J.: A linearization of the lambda-calculus and consequences. J. Logic Comput. 10(3), 411\u2013436 (2000)","journal-title":"J. Logic Comput."},{"issue":"1\u20133","key":"25_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2003.10.032","volume":"311","author":"AJ Kfoury","year":"2004","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311(1\u20133), 1\u201370 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR22","volume-title":"Lambda-Calculus, Types and Models","author":"J-L Krivine","year":"1993","unstructured":"Krivine, J.-L.: Lambda-Calculus, Types and Models. Ellis Horwood, Hemel Hempstead (1993)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Mairson, H., Neergaard, P.M.: Types, potency, idempotency: why nonlinearity and amnesia make a type system work. In: ICFP, pp. 138\u2013149. ACM (2004)","DOI":"10.1145\/1016848.1016871"},{"issue":"1\u20132","key":"25_CR24","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0304-3975(98)00358-2","volume":"228","author":"J Maraist","year":"1999","unstructured":"Maraist, J., Odersky, M., Turner, D.N., Wadler, P.: Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoret. Comput. Sci. 228(1\u20132), 175\u2013210 (1999)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"25_CR25","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":"25_CR26","doi-asserted-by":"crossref","first-page":"358","DOI":"10.3233\/FI-2010-324","volume":"103","author":"M Pagani","year":"2010","unstructured":"Pagani, M., Ronchi Della Rocca, S.: Linearity, non-determinism and solvability. Fundam. Informaticae 103, 358\u2013373 (2010)","journal-title":"Fundam. Informaticae"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-12032-9_25","volume-title":"Foundations of Software Science and Computational Structures","author":"M Pagani","year":"2010","unstructured":"Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 358\u2013373. Springer, Heidelberg (2010)"},{"issue":"2","key":"25_CR28","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-Name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S Bakel van","year":"1992","unstructured":"van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput. Sci. 102(1), 135\u2013163 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR30","unstructured":"Wadsworth, C.: Semantics and Pragmatics of the Lambda Calculus. PH.D. thesis, Oxford University (1971)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,23]],"date-time":"2020-03-23T21:08:35Z","timestamp":1584997715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_25","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}