{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:36Z","timestamp":1767928296842,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662494974","type":"print"},{"value":"9783662494981","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-49498-1_9","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T13:36:06Z","timestamp":1458567366000},"page":"202-228","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Call-By-Push-Value from a Linear Logic Point of View"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ehrhard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Benton, P.N., Wadler, P.: Linear logic, monads and the lambda calculus. In: Proceedings of 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27\u201330, pp. 420\u2013431. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561458"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/BFb0014046","volume-title":"Typed Lambda Calculi and Applications","author":"GM Bierman","year":"1995","unstructured":"Bierman, G.M.: What is a categorical model of intuitionistic linear logic? In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 78\u201393. Springer, Heidelberg (1995)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-54830-7_7","volume-title":"Foundations of Software Science and Computation Structures","author":"A Carraro","year":"2014","unstructured":"Carraro, A., Guerrieri, G.: A semantical and operational account of call-by-value solvability. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 103\u2013118. Springer, Heidelberg (2014)"},{"key":"9_CR5","unstructured":"Curien, P.-L.: Call-By-Push-Value in system L style. Unpublished note (2015)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Fiore, M., Munch-Maccagnoni, G.: A theory of effects and resources: adjunction models and polarised calculi. In: Proceedings of POpPL (2015, To appear) (2016)","DOI":"10.1145\/2837614.2837652"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Odersky, M., Wadler, P. (eds.) Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 18\u201321, pp. 233\u2013243. ACM (2000)","DOI":"10.1145\/351240.351262"},{"key":"9_CR8","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-15240-5_13","volume-title":"Theoretical Computer Science","author":"P-L Curien","year":"2010","unstructured":"Curien, P.-L., Munch-Maccagnoni, G.: The duality of computation under focus. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 165\u2013181. Springer, Heidelberg (2010)"},{"issue":"1","key":"9_CR9","first-page":"111","volume":"152","author":"V Danos","year":"2011","unstructured":"Danos, V., Ehrhard, T.: Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput. 152(1), 111\u2013137 (2011)","journal-title":"Inf. Comput."},{"issue":"3","key":"9_CR10","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1093\/logcom\/exs025","volume":"24","author":"J Egger","year":"2014","unstructured":"Egger, J., M\u00f8gelberg, R.E., Simpson, A.: The enriched effect calculus: syntax and semantics. J. Logic Comput. 24(3), 615\u2013654 (2014)","journal-title":"J. Logic Comput."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.tcs.2011.11.027","volume":"424","author":"T Ehrhard","year":"2012","unstructured":"Ehrhard, T.: The scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci. 424, 20\u201345 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Ehrhard, T., Tasson, C., Pagani, M.: Probabilistic coherence spaces are fully abstract for probabilistic PCF. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 309\u2013320. ACM (2014)","DOI":"10.1145\/2535838.2535865"},{"key":"9_CR13","unstructured":"Fiore, M.P., Plotkin, G.D.: An axiomatization of computationally adequate domain theoretic models of FPC. In: Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS 1994), Paris, France, July 4\u20137, pp. 92\u2013102. IEEE Computer Society (1994)"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J-Y Girard","year":"1991","unstructured":"Girard, J.-Y.: A new constructive logic: classical logic. Math. Struct. Comput. Sci. 1(3), 225\u2013296 (1991)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"3","key":"9_CR16","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J-Y Girard","year":"2001","unstructured":"Girard, J.-Y.: Locus solum. Math. Struct. Comput. Sci. 11(3), 301\u2013506 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-45788-7_10","volume-title":"Functional and Logic Programming","author":"M Hasegawa","year":"2002","unstructured":"Hasegawa, M.: Linearly used effects: monadic and CPS transformations into the linear lambda calculus. In: Hu, Z., Rodr\u00edguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol. 2441, pp. 167\u2013182. Springer, Heidelberg (2002)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-58027-1_21","volume-title":"Mathematical Foundations of Programming Semantics","author":"M Huth","year":"1994","unstructured":"Huth, M.: Linear domains and linear maps. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 438\u2013453. Springer, Heidelberg (1994)"},{"key":"9_CR19","unstructured":"Krivine, J.-L.: Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, Translation by Ren\u00e9 Cori from French 1990 (edn.) (Masson) (1993)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0304-3975(94)90081-7","volume":"129","author":"J-L Krivine","year":"1994","unstructured":"Krivine, J.-L.: A general storage theorem for integers in call-by-name $$\\lambda $$ \u03bb -calculus. Theor. Comput. Sci. 129, 79\u201394 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Laurent, O., Regnier, L.: About translations of classical logic into polarized linear logic. In: Proceedings of 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 22\u201325, Ottawa, Canada, pp. 11\u201320. IEEE Computer Society, June 2003","DOI":"10.1109\/LICS.2003.1210040"},{"key":"9_CR22","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/S1571-0661(04)80568-1","volume":"69","author":"PB Levy","year":"2002","unstructured":"Levy, P.B.: Adjunction models for call-by-push-value with stacks. Electron. Notes Theor. Comput. Sci. 69, 248\u2013271 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR23","series-title":"Semantics Structures in Computation","volume-title":"Call-By-Push-Value: A Functional\/Imperative Synthesis","author":"PB Levy","year":"2004","unstructured":"Levy, P.B.: Call-By-Push-Value: A Functional\/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Springer, Heidelberg (2004)"},{"issue":"1\u20132","key":"9_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. Theor. Comput. Sci. 228(1\u20132), 175\u2013210 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR25","unstructured":"Marz, M., Rohr, A., Streicher, T.: Full Abstraction and Universality via Realisability. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2\u20135, pp. 174\u2013182. IEEE Computer Society, (1999)"},{"key":"9_CR26","volume-title":"Interactive Models of Computation and Program Behaviour","author":"P-A Melli\u00e8s","year":"2009","unstructured":"Melli\u00e8s, P.-A.: Categorical semantics of linear logic. In: Curien, P.-L., Herbelin, H., Krivine, J.-L., Melli\u00e8s, P.-A. (eds.) Interactive Models of Computation and Program Behaviour, vol. 27. Panoramas et Synth\u00e8ses, Soci\u00e8t\u00e8 Math\u00e8matique de France, Marseille (2009)"},{"key":"9_CR27","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society (1989)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Seely, R.A.G.: Linear logic, *-autonomous categories and cofree coalgebras. Contem. Math. 92 (1989). American Mathematical Society","DOI":"10.1090\/conm\/092\/1003210"},{"issue":"2","key":"9_CR29","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. Math. Struct. Comput. Sci. 11(2), 207\u2013260 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Simpson, A.K., Plotkin, G.D.: Complete axioms for categorical fixed-point operators. In: 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, 26\u201329 June, pp. 30\u201341. IEEE Computer Society (2000)","DOI":"10.1109\/LICS.2000.855753"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-49253-4_6","volume-title":"Algebraic Methodology and Software Technology","author":"G Winskel","year":"1998","unstructured":"Winskel, G.: A linear metalanguage for concurrency. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 42\u201358. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:35:19Z","timestamp":1748813719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_9","relation":{},"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"}]}}