{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:48:26Z","timestamp":1770277706224,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255963","type":"print"},{"value":"9783540320333","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_15","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"185-203","source":"Crossref","is-referenced-by-count":16,"title":["Call-by-Value Is Dual to Call-by-Name \u2013 Reloaded"],"prefix":"10.1007","author":[{"given":"Philip","family":"Wadler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Ariola, Z., Herbelin, H.: Minimal classical logic and control operators. In: 30\u2019th International Colloquium on Automata, Languages and Programming, Eindhoven, The Netherlands (2003)","DOI":"10.1007\/3-540-45061-0_68"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Balat, V., Cosmo, R.D., Fiore, M.: Extensional normalisation and type-directed partial evaluation for typed lambda-calculus with sums. Principles of Programming Languages (2004)","DOI":"10.1145\/964001.964007"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Information and Computation\u00a0125(2), 103\u2013117 (1996)","journal-title":"Information and Computation"},{"key":"15_CR4","first-page":"74","volume":"1","author":"P. Bernays","year":"1936","unstructured":"Bernays, P.: Review of \u201cSome Properties of Conversion\u201d by Alonzo Church and J. B. Rosser. Journal of Symbolic Logic\u00a01, 74\u201375 (1936)","journal-title":"Journal of Symbolic Logic"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"346","DOI":"10.2307\/1968337","volume":"II.33","author":"A. Church","year":"1932","unstructured":"Church, A.: A set of postulates for the foundation of logic. Annals of Mathematics\u00a0II.33, 346\u2013366 (1932)","journal-title":"Annals of Mathematics"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"15_CR7","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1093\/logcom\/14.4.529","volume":"14","author":"T. Crolard","year":"2004","unstructured":"Crolard, T.: A formulae-as-types interpretation of Subtractive Logic. Journal of Logic and Computation\u00a014(4), 529\u2013570 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"15_CR8","first-page":"233","volume-title":"5\u2019th International Conference on Functional Programming","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: 5\u2019th International Conference on Functional Programming, September 2000, pp. 233\u2013243. ACM, New York (2000)"},{"key":"15_CR9","series-title":"London Mathematical Society Lecture Note Series","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 linear decomposition of classical implication. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Note Series, vol.\u00a0222, pp. 211\u2013224. Cambridge University Press, Cambridge (1995)"},{"key":"15_CR10","unstructured":"Filinski, A.: Declarative continuations and categorical duality. Master\u2019s thesis, University of Copenhagen, Copenhagen, Denmark, August 1989 (DIKU Report 89\/11) (1989)"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-44904-3_9","volume-title":"Typed Lambda Calculi and Applications","author":"K. Fujita","year":"2003","unstructured":"Fujita, K.: A Sound and Complete CPS-Translation for \u03bb\u03bc-Calculus. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 120\u2013134. Springer, Heidelberg (2003)"},{"key":"15_CR12","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Investigations into Logical Deduction. Mathematische Zeitschrift\u00a039, 176\u2013210 (1935) Reprinted in Szabo, M. E. (eds), The Collected Papers of Gerhard Gentzen, North-Holland (1969)","journal-title":"Mathematische Zeitschrift"},{"key":"15_CR13","volume-title":"17\u2019th Symposium on Principles of Programming Languages","author":"T. Griffin","year":"1990","unstructured":"Griffin, T.: A formulae-as-types notion of control. In: 17\u2019th Symposium on Principles of Programming Languages, San Francisco, CA, January 1990, ACM, New York (1990)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: Continuation models are universal for \u03bb\u03bc- calculus. In: Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, pp. 387\u2013397 (1997)","DOI":"10.1109\/LICS.1997.614964"},{"issue":"1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(94)00123-Z","volume":"136","author":"A. Melton","year":"1994","unstructured":"Melton, A., Schr\u00f6der, B.S.W., Strecker, G.E.: Lagois connections, a counterpart to Galois connections. Theoretical Computer Science\u00a0136(1), 79\u2013107 (1994)","journal-title":"Theoretical Computer Science"},{"key":"15_CR16","unstructured":"Moggi, E.: Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Edinburgh University, Department of Computer Science (1988)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L.: A semantic view of classical proofs: Type-theoretic, categorical, and denotational characterizations. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 230\u2013241 (1996)","DOI":"10.1109\/LICS.1996.561323"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Proceedings of the Symposium on Principles of Programming Languages, pp. 215\u2013227 (1997)","DOI":"10.1145\/263699.263722"},{"key":"15_CR19","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.: \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"15_CR20","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 \u03bb-calculus. Theoretical Computer Science\u00a01, 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/S0022-4049(00)00161-4","volume":"159","author":"D. Pym","year":"2001","unstructured":"Pym, D., Ritter, E.: On the Semantics of Classical Disjunction. Journal of Pure and Applied Algebra\u00a0159, 315\u2013338 (2001)","journal-title":"Journal of Pure and Applied Algebra"},{"issue":"3\/4","key":"15_CR22","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"},{"issue":"6","key":"15_CR23","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A. Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems\u00a019(6), 916\u2013941 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR24","unstructured":"Selinger, P.: Control categories and duality: an axiomatic approach to the semantics of functional control. In: Talk presented at Mathematical Foundations of Programming Semantics, London (May 1998)"},{"key":"15_CR25","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, 207\u2013260 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"6","key":"15_CR26","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1017\/S0956796898003141","volume":"8","author":"T. Streicher","year":"1998","unstructured":"Streicher, T., Reuss, B.: Classical logic, continuation semantics and abstract machines. Journal of Functional Programming\u00a08(6), 543\u2013572 (1998)","journal-title":"Journal of Functional Programming"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Call-by-name is dual to call-by-value. In: International Conference on Functional Programming, Uppsala, Sweden (August 25-29, 2003)","DOI":"10.1145\/944705.944723"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:33:57Z","timestamp":1605760437000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}