{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:46Z","timestamp":1763468026725},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642216909"},{"type":"electronic","value":"9783642216916"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21691-6_6","type":"book-chapter","created":{"date-parts":[[2011,6,11]],"date-time":"2011-06-11T05:31:26Z","timestamp":1307770286000},"page":"27-44","source":"Crossref","is-referenced-by-count":9,"title":["Classical Call-by-Need and Duality"],"prefix":"10.1007","author":[{"given":"Zena M.","family":"Ariola","sequence":"first","affiliation":[]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"Z. Ariola","year":"2003","unstructured":"Ariola, Z., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, Springer, Heidelberg (2003)"},{"issue":"4","key":"6_CR2","first-page":"275","volume":"31","author":"Z.M. Ariola","year":"2009","unstructured":"Ariola, Z.M., Bohannon, A., Sabry, A.: Sequent calculi and abstract machines. Transactions on Programming Languages and Systems (TOPLAS)\u00a031(4), 275\u2013317 (2009)","journal-title":"Transactions on Programming Languages and Systems (TOPLAS)"},{"issue":"3","key":"6_CR3","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"Z.M. Ariola","year":"1997","unstructured":"Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program.\u00a07(3), 265\u2013301 (1997)","journal-title":"J. Funct. Program."},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1017\/S0956796807006612","volume":"18","author":"Z.M. Ariola","year":"2008","unstructured":"Ariola, Z.M., Herbelin, H.: Control reduction theories: the benefit of structural substitution. J. Funct. Program.\u00a018(3), 373\u2013419 (2008)","journal-title":"J. Funct. Program."},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s10990-007-9007-z","volume":"20","author":"Z.M. Ariola","year":"2007","unstructured":"Ariola, Z.M., Herbelin, H., Sabry, A.: A proof-theoretic foundation of abortive continuations. Higher Order Symbol. Comput.\u00a020, 403\u2013429 (2007)","journal-title":"Higher Order Symbol. Comput."},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/s10990-007-9006-0","volume":"22","author":"Z.M. Ariola","year":"2009","unstructured":"Ariola, Z.M., Herbelin, H., Sabry, A.: A type-theoretic foundation of delimited continuations. Higher Order Symbol. Comput.\u00a022, 233\u2013273 (2009)","journal-title":"Higher Order Symbol. Comput."},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H. Barendregt","year":"2000","unstructured":"Barendregt, H., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program.\u00a010, 121\u2013134 (2000)","journal-title":"J. Funct. Program."},{"key":"6_CR8","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)"},{"issue":"33","key":"6_CR9","doi-asserted-by":"publisher","first-page":"346","DOI":"10.2307\/1968337","volume":"2","author":"A. Church","year":"1932","unstructured":"Church, A.: A set of postulates for the foundation of logic. Annals of Mathematics\u00a02(33), 346\u2013366 (1932)","journal-title":"Annals of Mathematics"},{"issue":"1-2","key":"6_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","volume":"254","author":"T. Crolard","year":"2001","unstructured":"Crolard, T.: Subtractive Logic. Theoretical Computer Science\u00a0254(1-2), 151\u2013185 (2001)","journal-title":"Theoretical Computer Science"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: International Conference on Functional Programming, pp. 233\u2013243 (2000)","DOI":"10.1145\/351240.351262"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1017\/CBO9780511629150.011","volume-title":"Advances in Linear Logic","author":"V. Danos","year":"1995","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication. In: Advances in Linear Logic, vol.\u00a0222, pp. 211\u2013224. Cambridge University Press, Cambridge (1995)"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. J. Symb. Log.\u00a062(3), 755\u2013807 (1997)","journal-title":"J. Symb. Log."},{"key":"6_CR14","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.\u00a06009, pp. 240\u2013256. Springer, Heidelberg (2010)"},{"issue":"1","key":"6_CR15","doi-asserted-by":"publisher","first-page":"407","DOI":"10.2307\/2694930","volume":"66","author":"R. David","year":"2001","unstructured":"David, R., Py, W.: Lambda-mu-calculus and B\u00f6hm\u2019s theorem. J. Symb. Log.\u00a066(1), 407\u2013413 (2001)","journal-title":"J. Symb. Log."},{"key":"6_CR16","unstructured":"Fasel, J.H., Hudak, P., Peyton Jones, S., Wadler, P. (eds.): Haskell special issue. SIGPLAN Notices\u00a027(5) (May 1992)"},{"key":"6_CR17","first-page":"193","volume-title":"Formal Description of Programming Concepts-III","author":"M. Felleisen","year":"1986","unstructured":"Felleisen, M., Friedman, D.: Control operators, the secd machine, and the lambda-calculus. In: Formal Description of Programming Concepts-III, pp. 193\u2013217. North-Holland, Amsterdam (1986)"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","volume":"52","author":"M. Felleisen","year":"1987","unstructured":"Felleisen, M., Friedman, D., Kohlbecker, E.: A syntactic theory of sequential control. Theoretical Computer Science\u00a052(3), 205\u2013237 (1987)","journal-title":"Theoretical Computer Science"},{"key":"6_CR19","unstructured":"Felleisen, M., Friedman, D., Kohlbecker, E., Duba, B.: Reasoning with continuations. In: First Symposium on Logic and Computer Science, pp. 131\u2013141 (1986)"},{"key":"6_CR20","unstructured":"Filinski, A.: Declarative Continuations and Categorical Duality. Master thesis, DIKU, Danmark (August 1989)"},{"key":"6_CR21","first-page":"153","volume-title":"POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"R. Garcia","year":"2009","unstructured":"Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. In: POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 153\u2013164. ACM, New York (2009)"},{"key":"6_CR22","first-page":"68","volume-title":"Collected papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M. (ed.) Collected papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1969)"},{"key":"6_CR23","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule. In: Habilitation \u00e0 diriger les reserches (2005)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-02273-9_12","volume-title":"Typed Lambda Calculi and Applications","author":"H. Herbelin","year":"2009","unstructured":"Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical \u03bb-calculus in \u201cnatural deduction\u201d form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 142\u2013156. Springer, Heidelberg (2009)"},{"key":"6_CR25","unstructured":"Lafont, Y., Reus, B., Streicher, T.: Continuations semantics or expressing implication by negation. Technical Report 9321, Ludwig-Maximilians-Universit\u00c3d\u2019t, M\u00c3ijnchen (1993)"},{"issue":"3","key":"6_CR26","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 \u03bb-calculus. J. Funct. Program.\u00a08(3), 275\u2013317 (1998)","journal-title":"J. Funct. Program."},{"key":"6_CR27","unstructured":"Moggi, E.: Computational \u03bb-calculus and monads. In: Logic in Computer Science (1989)"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/j.tcs.2006.08.016","volume":"364","author":"J. Niehren","year":"2006","unstructured":"Niehren, J., Schwinghammer, J., Smolka, G.: A concurrent lambda calculus with futures. Theor. Comput. Sci.\u00a0364, 338\u2013356 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR29","first-page":"57","volume-title":"Lisp and Symbolic Computation","author":"C. Okasaki","year":"1993","unstructured":"Okasaki, C., Lee, P., Tarditi, D.: Call-by-need and continuation-passing style. In: Lisp and Symbolic Computation, pp. 57\u201381. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"6_CR30","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.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"6_CR31","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Comput. Sci.\u00a01, 125\u2013159 (1975)","journal-title":"Theoretical Comput. Sci."},{"key":"6_CR32","volume-title":"Natural Deduction, a Proof-Theoretical Study","author":"D. Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction, a Proof-Theoretical Study. Almquist and Wiksell, Stockholm (1965)"},{"key":"6_CR33","series-title":"Texts in Theoretical Computer Science: An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10394-4","volume-title":"The Parametric \u03bb-Calculus: a Metamodel for Computation","author":"S. Ronchi Della Rocca","year":"2004","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The Parametric \u03bb-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer, Heidelberg (2004)"},{"issue":"3-4","key":"6_CR34","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A. Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation\u00a06(3-4), 289\u2013360 (1993)","journal-title":"Lisp and Symbolic Computation"},{"key":"6_CR35","first-page":"356","volume-title":"Proceedings of 20th IEEE Symposium on Logic in Computer Science (LICS 2005)","author":"A. Saurin","year":"2005","unstructured":"Saurin, A.: Separation with streams in the \u03bb\u03bc-calculus. In: Proceedings of 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, June 26-29, pp. 356\u2013365. IEEE Computer Society, Los Alamitos (2005)"},{"issue":"2","key":"6_CR36","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1017\/S096012950000311X","volume":"11","author":"P. Selinger","year":"2001","unstructured":"Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. Mathematical Structures in Computer Science\u00a011(2), 207\u2013260 (2001)","journal-title":"Mathematical Structures in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21691-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,28]],"date-time":"2019-03-28T16:07:27Z","timestamp":1553789247000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21691-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642216909","9783642216916"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21691-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}