{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:56Z","timestamp":1775790776826,"version":"3.50.1"},"reference-count":37,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":6784,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1016\/s1571-0661(04)00022-2","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T05:14:39Z","timestamp":1075353279000},"page":"370-392","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":24,"special_numbering":"C","title":["Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus"],"prefix":"10.1016","volume":"1","author":[{"given":"John","family":"Maraist","sequence":"first","affiliation":[]},{"given":"Martin","family":"Odersky","sequence":"additional","affiliation":[]},{"given":"David N.","family":"Turner","sequence":"additional","affiliation":[]},{"given":"Philip","family":"Wadler","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","article-title":"Computational interpretations of linear logic","volume":"111","author":"Abramsky","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB2","series-title":"Principles of Programming Languages (POPL)","article-title":"A call-by-need lambda calculus","author":"Ariola","year":"1995"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB3","unstructured":"Z. M. Ariola and M. Felleisen, The call-by-need lambda calculus. Technical report CIS-TR-94-23, Department of Computer Science, University of Oregon, October 1994."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB4","unstructured":"Z. M. Ariola and J. W. Klop, Cyclic lambda graph rewriting. In Logic in Computer Science (LICS), Paris, France, 1994"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB5","series-title":"The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Computer Science","author":"Barendregt","year":"1981"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB6","doi-asserted-by":"crossref","unstructured":"N. Benton, G. Bierman, V. de Paiva, and M. Hyland, Type assignment for intuitionistic linear logic. Technical report 262, Computing Laboratory, University of Cambridge, August 1992.","DOI":"10.1007\/BFb0037099"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB7","unstructured":"P. N. Benton, Strong normalisation for the linear term calculus. Technical report 305, Computing Laboratory, University of Cambridge, July 1993. To appear in Journal of Functional Programming."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB8","doi-asserted-by":"crossref","unstructured":"G. Bierman, What is a categorical model of intuitionistic linear logic? Technical report 333, Computing Laboratory, University of Cambridge, April 1994. To appear in Proceedings of the Conference on Typed Lambda Calculus and Applications, Springer Verlag LNCS, April 1995.","DOI":"10.1007\/BFb0014046"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB9","unstructured":"G. Bierman, On Intuitionistic Linear Logic. Technical report 346, Computing Laboratory, University of Cambridge, August 1994."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB10","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt and K. Hemerik, Types in Lambda Calculus and Programming Languages. In European Symposium on Programming (ESOP), p. 1\u201335. Springer-Verlag, Lecture Notes in Computer Science 432, 1990.","DOI":"10.1007\/3-540-52592-0_53"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","article-title":"On the unity of logic","volume":"59","author":"Girard","year":"1993","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB13","series-title":"Principles of Programming Languages (POPL)","article-title":"The geometry of optimal lambda reduction","author":"Gonthier","year":"1992"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB14","unstructured":"S. Holmstr\u00f6m, A linear functional language. Draft paper, Chalmers University of Technology, 1988."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB15","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0168-0072(94)90020-5","article-title":"Semantics of weakening and contraction","volume":"69","author":"Jacobs","year":"1994","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB16","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","article-title":"The linear abstract machine","volume":"59","author":"Lafont","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB17","doi-asserted-by":"crossref","unstructured":"J. Launchbury, A natural semantics for lazy evaluation, Symposium on Principles of Programming Languages, ACM Press, Charleston, South Carolina, January 1993.","DOI":"10.1145\/158511.158618"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB18","unstructured":"P. Lincoln and J. Mitchell, Operational aspects of linear lambda calculus. In 7'th Symposium on Logic in Computer Science, IEEE Press, Santa Cruz, California, June 1992."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB19","unstructured":"I. Mackie, Lilac: a functional programming language based on linear logic. Master's Thesis, Imperial College London, 1991."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB20","unstructured":"I. Mackie, The Geometry of Implementation. Doctoral Thesis, Imperial College London, 1994."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB21","unstructured":"E. Moggi, Computational lambda-calculus and monads. Technical report ECS-LFCS-88-66, Laboratory for the Foundations of Computer Science, University of Edinburgh, October 1988."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB22","unstructured":"E. Moggi, Computational lambda-calculus and monads. In 4'th Symposium on Logic in Computer Science, IEEE Press, Asilomar, California, June 1989."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB23","doi-asserted-by":"crossref","unstructured":"J. Maraist, M. Odersky, D. N. Turner, and P. Wadler, Call-by-name, call-by-value, call-by-need, and the linear lambda calculus. Technical report, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe and Department of Computing Science, University of Glasgow, March 1995.","DOI":"10.1016\/S1571-0661(04)00022-2"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB24","unstructured":"J. Maraist, M. Odersky, and P. Wadler, The call-by-need lambda calculus, Technical report, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, and Department of Computing Science, University of Glasgow, October 1994."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB25","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value, and the lambda calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB26","unstructured":"G. D. Plotkin, Private communication. (During the 1993 MFPS, even!)"},{"issue":"3\/4","key":"10.1016\/S1571-0661(04)00022-2_NEWBIB27","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF01019459","article-title":"The discoveries of continuations","volume":"6","author":"Reynolds","year":"1993","journal-title":"Lisp and Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB28","unstructured":"S. R. della Rocca and L. Roversi, Lambda calculus and intuitionistic linear logic. Manuscript, July 1994. (Available from L. Roversi, University of Pisa, rover@di.unipi.it.)"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB29","unstructured":"H. Schellinx, The noble art of linear decorating. Ph.D. dissertation, Institute for Logic, Language, and Computation, University of Amsterdam, 1994."},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB30","doi-asserted-by":"crossref","unstructured":"R. A. G. Seely, Linear logic, \u2217-autonomous categories, and cofree coalgebras. In Categories in Computer Science and Logic, June 1989. AMS Contemporary Mathematics 92.","DOI":"10.1090\/conm\/092\/1003210"},{"issue":"3\/4","key":"10.1016\/S1571-0661(04)00022-2_NEWBIB31","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01019462","article-title":"Reasoning about programs in continuation-passing style","volume":"6","author":"Sabry","year":"1993","journal-title":"Lisp and Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB32","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra, Lectures on Linear Logic. CSLI Lecture Notes, 1992.","DOI":"10.1093\/oso\/9780198537779.003.0013"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB33","doi-asserted-by":"crossref","unstructured":"D. N. Turner, P. Wadler, and C. Mossin, Once upon a type. In Functional Programming and Computer Architecture (FPCA), San Diego, California, June 1995.","DOI":"10.1145\/224164.224168"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB34","series-title":"Programming Concepts and Methods","article-title":"Linear types can change the world!","author":"Wadler","year":"1990"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB35","series-title":"Partial Evaluation and Semantics-Based Program Manipulation (PEPM)","article-title":"Is there a use for linear logic?","author":"Wadler","year":"1991"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB36","doi-asserted-by":"crossref","unstructured":"P. Wadler, A syntax for linear logic. Ninth International Conference on the Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1993. Springer Verlag, LNCS 802.","DOI":"10.1007\/3-540-58027-1_24"},{"key":"10.1016\/S1571-0661(04)00022-2_NEWBIB37","series-title":"Mathematical Foundations of Computer Science","article-title":"A taste of linear logic","author":"Wadler","year":"1993"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000222?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000222?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:03:01Z","timestamp":1761609781000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104000222"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":37,"alternative-id":["S1571066104000222"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00022-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)00022-2","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}