{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T14:15:54Z","timestamp":1770041754227,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T00:00:00Z","timestamp":1164931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2006,12]]},"DOI":"10.1007\/s10990-006-0480-6","type":"journal-article","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T18:07:57Z","timestamp":1164650877000},"page":"377-414","source":"Crossref","is-referenced-by-count":51,"title":["Call-by-push-value: Decomposing call-by-value and call-by-name"],"prefix":"10.1007","volume":"19","author":[{"given":"Paul Blain","family":"Levy","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"480_CR1","unstructured":"Abramsky, S.: The lazy \u03bb-Calculus. In Research Topics in Functional Programming. Addison Wesley, pp. 65\u2013117 (1990)"},{"key":"480_CR2","volume-title":"The Lambda-Calculus: Its Syntax and Semantics.","author":"H. Barendregt","year":"1980","unstructured":"Barendregt, H.: The Lambda-Calculus: Its Syntax and Semantics. North-Holland, Amsterdam (1980)"},{"key":"480_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.), Advanced Lectures From International Summer School on Applied Semantics (APPSEM), Caminha, Portugal, vol. 2395 of Lecture Notes in Computer Science, pp. 42\u2013122 (2000)","DOI":"10.1007\/3-540-45699-6_2"},{"key":"480_CR4","doi-asserted-by":"crossref","unstructured":"Benton, N., Kennedy, A.: Monads, effects and transformations. In: Gordon, A., Pitts, A. (eds.), Proceedings, Higher-Order Operational Techniques in Semantics (HOOTS \u201999), vol. 26 of ENTCS, Paris, France, pp. 3\u201320 (1999)","DOI":"10.1016\/S1571-0661(05)80280-4"},{"key":"480_CR5","doi-asserted-by":"crossref","unstructured":"Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, IEEE Computer Society Press, pp. 420\u2013431 (1996)","DOI":"10.1109\/LICS.1996.561458"},{"key":"480_CR6","unstructured":"Felleisen, M., Friedman, D.: Control operators, the SECD-machine, and the \u03bb-calculus. In: Wirsing, M. (ed.), Formal Description of Programming Concepts III, North-Holland, pp. 193\u2013217 (1986)"},{"key":"480_CR7","unstructured":"Filinski, A.: Controlling Effects. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania (1996)"},{"key":"480_CR8","doi-asserted-by":"crossref","unstructured":"F\u00fchrmann, C.: Direct models for the computational \u03bb-calculus. In: Brookes, S., Jung, A., Mislove, M., Scedrov, A. (eds.), In: Proceedings of the 15th Conference in Mathematical Foundations of Programming Semantics, New Orleans, vol. 20 of ENTCS, pp. 147\u2013172 (1999).","DOI":"10.1016\/S1571-0661(04)80078-1"},{"key":"480_CR9","doi-asserted-by":"crossref","unstructured":"Hatcliff, J.: The Structure of Continuation-Passing Styles. PhD thesis, Kansas State University, (1994)","DOI":"10.1145\/174675.178053"},{"issue":"3","key":"480_CR10","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1017\/S0956796897002748","volume":"7","author":"J. Hatcliff","year":"1997","unstructured":"Hatcliff, J., Danvy, O.: Thunks and the \u03bb-calculus. Journal of Functional Programming, 7(3), 303\u2013319 (1997)","journal-title":"Journal of Functional Programming"},{"key":"480_CR11","doi-asserted-by":"crossref","unstructured":"Howard, B.: Inductive, coinductive, and pointed types. In: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP \u201996), vol. 31, no. 6 of ACM SIGPLAN Notices, pp. 102\u2013109. ACM, (1996)","DOI":"10.1145\/232627.232640"},{"issue":"1\u20132","key":"480_CR12","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0304-3975(98)00356-9","volume":"228","author":"A. Jeffrey","year":"1999","unstructured":"Jeffrey, A.: A fully abstract semantics for a higher-order functional language with nondeterministic computation. Theoretical Computer Science, 228(1\u20132), 105\u2013150 (1999)","journal-title":"Theoretical Computer Science"},{"key":"480_CR13","unstructured":"Krivine, J.-L.: Un interpr\u00e9teur de \u03bb-calcul. Unpublished, (1985)"},{"key":"480_CR14","unstructured":"Laird, J.: A Semantic Analysis of Control. PhD thesis, University of Edinburgh (1998)"},{"key":"480_CR15","doi-asserted-by":"crossref","unstructured":"Laurent, O.: Polarized proof-nets: proof-nets for LC (extended abstract). In: Girard, J.-Y. (ed.), Typed Lambda Calculi and Applications \u201999, L\u2019Aquila, Italy, vol. 1581 of Lecture Notes in Computer Science, pp. 213\u2013227. Springer (1999)","DOI":"10.1007\/3-540-48959-2_16"},{"key":"480_CR16","unstructured":"Levy, P.B.: \u03bb-calculus and cartesian closed categories. Essay for Part III of the Mathematical Tripos, Cambridge University (1996)"},{"key":"480_CR17","doi-asserted-by":"crossref","unstructured":"Levy, P.B.: Call-by-push-value: a subsuming paradigm (extended abstract). In: Girard, J.-Y (ed.), In: Proceedings, Typed Lambda-Calculi and Applications, L\u2019Aquila, Italy, vol. 1581 of LNCS, pp. 228\u2013242. Springer (1999)","DOI":"10.1007\/3-540-48959-2_17"},{"key":"480_CR18","doi-asserted-by":"crossref","unstructured":"Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J. (ed.), In: Proceedings, 16th Annual Conference of the European Assocation for Computer Science Logic (CSL), vol. 2471 of LNCS, pp. 232\u2013246. Springer (2002)","DOI":"10.1007\/3-540-45793-3_16"},{"key":"480_CR19","doi-asserted-by":"crossref","unstructured":"Levy, P.B.: Adjunction models for call-by-push-value with stacks. In: Blute, R., Selinger, P. (eds.), In: Proceedings, 9th Conference on Category Theory and Computer Science, Ottawa, 2002, vol. 69 of Electronic Notes in Theoretical Computer Science (2003)","DOI":"10.1016\/S1571-0661(04)80568-1"},{"key":"480_CR20","unstructured":"Levy, P.B.: Call-By-Push-Value. A Functional\/Imperative Synthesis. Semantic Structures in Computation. Springer (2004)"},{"key":"480_CR21","first-page":"75","volume":"14","author":"P.B. Levy","year":"2005","unstructured":"Levy, P.B.: Adjunction models for call-by-push-value with stacks. Theory and Applications of Categories, 14, 75\u2013110 (2005)","journal-title":"Theory and Applications of Categories"},{"key":"480_CR22","doi-asserted-by":"crossref","unstructured":"Levy, P.B.: Jumbo \u03bb-calculus. In: Proceedings, 33rd International Colloquium on Automata, Languages and Programming, vol. 4052 of LNCS pp. 444\u2013455. Springer (2006)","DOI":"10.1007\/11787006_38"},{"key":"480_CR23","unstructured":"Marz, M.: A fully abstract model for sequential computation. Technical Report CSR-98-6, University of Birmingham, School of Computer Science (1998)"},{"key":"480_CR24","doi-asserted-by":"crossref","unstructured":"Marz, M.: A Fully Abstract Model for Sequential Computation. PhD thesis, Technische Universit\u00e4t Darmstadt, published by Logos-Verlag, Berlin (2000)","DOI":"10.1016\/S1571-0661(05)01206-5"},{"key":"480_CR25","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings, 4th Annual Symposium on Logic in Computer Science, Pacific Grove, California, pp. 14\u201323. IEEE (1989)","DOI":"10.1109\/LICS.1989.39155"},{"key":"480_CR26","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation 93, 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"480_CR27","unstructured":"O\u2019Hearn, P.W.: Opaque types in algol-like languages. Manuscript (1993)"},{"key":"480_CR28","unstructured":"Ong, C.H.L.: The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College of Science and Technology (1988)"},{"issue":"1","key":"480_CR29","doi-asserted-by":"crossref","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 1(1), 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"key":"480_CR30","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G.D. Plotkin","year":"1977","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theoretical Computer Science 5, 223\u2013255 (1977)","journal-title":"Theoretical Computer Science"},{"key":"480_CR31","unstructured":"Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 227\u2013273. Cambridge University Press (1998)"},{"issue":"2","key":"480_CR32","doi-asserted-by":"crossref","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 \u03bb\u03bc-calculus. Mathematical Structures in Computer Science 11(2), 207\u2013260 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"6","key":"480_CR33","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1017\/S0956796898003141","volume":"8","author":"Th. Streicher","year":"1998","unstructured":"Streicher, Th., Reus, B.: Classical logic, continuation semantics and abstract machines. Journal of Functional Programming 8(6), 543\u2013572 (1998)","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"480_CR34","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic 32(2), 198\u2013212 (1967)","journal-title":"Journal of Symbolic Logic"},{"key":"480_CR35","doi-asserted-by":"crossref","unstructured":"Winskel, G.: Formal Semantics of Programming Languages. MIT Press (1993)","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-006-0480-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-006-0480-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-006-0480-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T03:38:49Z","timestamp":1587267529000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-006-0480-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12]]}},"alternative-id":["480"],"URL":"https:\/\/doi.org\/10.1007\/s10990-006-0480-6","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}