{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:20Z","timestamp":1775790800065,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837652","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"44-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["A theory of effects and resources: adjunction models and polarised calculi"],"prefix":"10.1145","author":[{"given":"Pierre-Louis","family":"Curien","sequence":"first","affiliation":[{"name":"University of Paris Diderot, France \/ Inria, France"}]},{"given":"Marcelo","family":"Fiore","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Guillaume","family":"Munch-Maccagnoni","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016860"},{"key":"e_1_3_2_1_3_1","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt Hendrik Pieter","year":"1993","unstructured":"Hendrik Pieter Barendregt , Handbook of Logic in Computer Science , vol. 2 , ch. Lambda Calculi with Types, Oxford University Press , 1993 . Hendrik Pieter Barendregt, Handbook of Logic in Computer Science, vol. 2, ch. Lambda Calculi with Types, Oxford University Press, 1993."},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. CSL","author":"Benton Nick","year":"1994","unstructured":"Nick Benton , A mixed linear and non-linear logic: proofs, terms and models , Proc. CSL , Lecture Notes in Computer Science , vol. 933 , Springer-Verlag , 1994 . Nick Benton, A mixed linear and non-linear logic: proofs, terms and models, Proc. CSL, Lecture Notes in Computer Science, vol. 933, Springer-Verlag, 1994."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671430"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. LICS","author":"Benton Nick","year":"1996","unstructured":"Nick Benton and Philip Wadler , Linear Logic, Monads, and the Lambda Calculus , Proc. LICS , IEEE Computer Society Press , 1996 . Nick Benton and Philip Wadler, Linear Logic, Monads, and the Lambda Calculus, Proc. LICS, IEEE Computer Society Press, 1996."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671586"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.049"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"e_1_3_2_1_12_1","first-page":"222","article-title":"sequent calculi for second order logic based upon dual linear decompositions of the classical implication","volume":"1","author":"Danos Vincent","year":"1995","unstructured":"Vincent Danos , Jean-Baptiste Joinet , and Harold Schellinx , LKQ and LKT : sequent calculi for second order logic based upon dual linear decompositions of the classical implication , London Mathematical Society Lecture Notes 1 ( 1995 ), 222 . Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of the classical implication, London Mathematical Society Lecture Notes 1 (1995), 222.","journal-title":"London Mathematical Society Lecture Notes"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Mathematics","volume-title":"On closed categories of functors","author":"Day Brian","year":"1970","unstructured":"Brian Day , On closed categories of functors , Lecture Notes in Mathematics ( 1970 ), no. 137, 1\u201338. Brian Day, On closed categories of functors, Lecture Notes in Mathematics (1970), no. 137, 1\u201338."},{"key":"e_1_3_2_1_15_1","first-page":"210","article-title":"Limits of small functors","author":"Day Brian","year":"2007","unstructured":"Brian Day and Stephen Lack , Limits of small functors , Journal of Pure and Applied Algebra ( 2007 ), no. 210 , 651\u2013663. Brian Day and Stephen Lack, Limits of small functors, Journal of Pure and Applied Algebra (2007), no. 210, 651\u2013663.","journal-title":"Journal of Pure and Applied Algebra ("},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs025"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143174"},{"key":"e_1_3_2_1_18_1","unstructured":"Marcelo Fiore Linearising Call-By-Push-Value Note July 2011.  Marcelo Fiore Linearising Call-By-Push-Value Note July 2011."},{"key":"e_1_3_2_1_19_1","first-page":"156","volume-title":"Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types, Proc. LICS","author":"Fiore Marcelo","year":"2002","unstructured":"Marcelo Fiore , Roberto Di Cosmo, and Vincent Balat , Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types, Proc. LICS , IEEE Computer Society Press , 2002 , pp. 147\u2013 156 . Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat, Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types, Proc. LICS, IEEE Computer Society Press, 2002, pp. 147\u2013156."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80078-1"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000049"},{"key":"e_1_3_2_1_24_1","volume-title":"The Blind Spot: Lectures on Logic","year":"2011","unstructured":", The Blind Spot: Lectures on Logic , European Mathematical Society , 2011 . , The Blind Spot: Lectures on Logic, European Mathematical Society, 2011."},{"key":"e_1_3_2_1_25_1","first-page":"43","article-title":"Max Kelly, A universal property of the convolution monoidal structure","author":"Im Geun Bin","year":"1986","unstructured":"Geun Bin Im and G . Max Kelly, A universal property of the convolution monoidal structure , Journal of Pure and Applied Algebra ( 1986 ), no. 43 , 75\u201388. Geun Bin Im and G. Max Kelly, A universal property of the convolution monoidal structure, Journal of Pure and Applied Algebra (1986), no. 43, 75\u201388.","journal-title":"Journal of Pure and Applied Algebra ("},{"key":"e_1_3_2_1_26_1","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0063096","volume-title":"Doctrinal adjunction","author":"Kelly G. Max","year":"1974","unstructured":"G. Max Kelly , Doctrinal adjunction , Lecture Notes in Mathematics ( 1974 ), no. 420, 257\u2013280. G. Max Kelly, Doctrinal adjunction, Lecture Notes in Mathematics (1974), no. 420, 257\u2013280."},{"key":"e_1_3_2_1_27_1","series-title":"Lecture Notes in Mathematics 64","volume-title":"Basic Concepts of Enriched Category Theory","year":"1982","unstructured":", Basic Concepts of Enriched Category Theory , Lecture Notes in Mathematics 64 , Cambridge University Press , 1982 , Republished in: Reprints in Theory and Applications of Categories, No. 10 (2005) pp. 1\u2013136. , Basic Concepts of Enriched Category Theory, Lecture Notes in Mathematics 64, Cambridge University Press, 1982, Republished in: Reprints in Theory and Applications of Categories, No. 10 (2005) pp. 1\u2013136."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_3_2_1_29_1","volume-title":"Tech. report","author":"Lafont Yves","year":"1993","unstructured":"Yves Lafont , B. Reus , and Thomas Streicher , Continuation Semantics or Expressing Implication by Negation , Tech. report , University of Munich , 1993 . Yves Lafont, B. Reus, and Thomas Streicher, Continuation Semantics or Expressing Implication by Negation, Tech. report, University of Munich, 1993."},{"key":"e_1_3_2_1_30_1","volume-title":"Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II, mar","author":"Laurent Olivier","year":"2002","unstructured":"Olivier Laurent , Etude de la polarisation en logique , Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II, mar 2002 . Olivier Laurent, Etude de la polarisation en logique, Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille II, mar 2002."},{"key":"e_1_3_2_1_31_1","volume-title":"Semantic Structures in Computation","author":"Levy Paul Blain","year":"2004","unstructured":"Paul Blain Levy , Call-By-Push-Value : A Functional\/Imperative Synthesis , Semantic Structures in Computation , vol. 2 , Springer , 2004 . Paul Blain Levy, Call-By-Push-Value: A Functional\/Imperative Synthesis, Semantic Structures in Computation, vol. 2, Springer, 2004."},{"key":"e_1_3_2_1_32_1","first-page":"5","article-title":"Adjunction models for Call-by-Push-Value with stacks","volume":"14","year":"2005","unstructured":", Adjunction models for Call-by-Push-Value with stacks , Theory and Applications of Categories 14 ( 2005 ), no. 5 , 75\u2013110. , Adjunction models for Call-by-Push-Value with stacks, Theory and Applications of Categories 14 (2005), no. 5, 75\u2013110.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_1_33_1","first-page":"161","article-title":"Resource modalities in tensor logic","volume":"5","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2010","unstructured":"Paul-Andr\u00e9 Melli\u00e8s and Nicolas Tabareau , Resource modalities in tensor logic , Annals of Pure and Applied Logic 5 ( 2010 ), no. 161 , 632\u2013 653. Paul-Andr\u00e9 Melli\u00e8s and Nicolas Tabareau, Resource modalities in tensor logic, Annals of Pure and Applied Logic 5 (2010), no. 161, 632\u2013 653.","journal-title":"Annals of Pure and Applied Logic"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_36_1","volume-title":"Proc. CSL, LNCS","author":"Munch-Maccagnoni Guillaume","year":"2009","unstructured":"Guillaume Munch-Maccagnoni , Focalisation and Classical Realisability , Proc. CSL, LNCS , Springer-Verlag , 2009 . Guillaume Munch-Maccagnoni, Focalisation and Classical Realisability, Proc. CSL, LNCS, Springer-Verlag, 2009."},{"key":"e_1_3_2_1_37_1","unstructured":"Syntax and Models of a non-Associative Composition of Programs and Proofs Ph.D. thesis Univ. Paris Diderot 2013\n  . Syntax and Models of a non-Associative Composition of Programs and Proofs Ph.D. thesis Univ. Paris Diderot 2013."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603156"},{"key":"e_1_3_2_1_39_1","first-page":"412","volume-title":"Proc. FoSSaCS","year":"2014","unstructured":", Models of a Non-Associative Composition , Proc. FoSSaCS (A. Muscholl, ed.), LNCS, vol. 8412 , Springer , 2014 , pp. 397\u2013 412 . , Models of a Non-Associative Composition, Proc. FoSSaCS (A. Muscholl, ed.), LNCS, vol. 8412, Springer, 2014, pp. 397\u2013412."},{"key":"e_1_3_2_1_40_1","volume-title":"Proc. LICS 2015","author":"Munch-Maccagnoni Guillaume","year":"2015","unstructured":"Guillaume Munch-Maccagnoni and Gabriel Scherer , Polarised Intermediate Representation of Lambda Calculus with Sums , Proc. LICS 2015 , 2015 . Guillaume Munch-Maccagnoni and Gabriel Scherer, Polarised Intermediate Representation of Lambda Calculus with Sums, Proc. LICS 2015, 2015."},{"key":"e_1_3_2_1_41_1","first-page":"101","volume-title":"Proc. LICS","author":"Murthy Chetan R.","year":"1992","unstructured":"Chetan R. Murthy , A Computational Analysis of Girard\u2019s Translation and LC , Proc. LICS , 1992 , pp. 90\u2013 101 . Chetan R. Murthy, A Computational Analysis of Girard\u2019s Translation and LC, Proc. LICS, 1992, pp. 90\u2013101."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002375"},{"key":"e_1_3_2_1_43_1","first-page":"382","volume-title":"Conference on Categories in Computer Science and Logic, AMS Contemporary Mathematics","volume":"92","author":"Seely Robert","year":"1989","unstructured":"Robert Seely , Linear logic, *-autonomous categories and cofree algebras , Conference on Categories in Computer Science and Logic, AMS Contemporary Mathematics , vol. 92 , 1989 , pp. 371\u2013 382 . Robert Seely, Linear logic, *-autonomous categories and cofree algebras, Conference on Categories in Computer Science and Logic, AMS Contemporary Mathematics, vol. 92, 1989, pp. 371\u2013382."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"e_1_3_2_1_45_1","volume-title":"International Workshop on the Mathematical Foundations of Programming Semantics","author":"Wadler Philip","year":"1992","unstructured":"Philip Wadler , There\u2019s no substitute for linear logic, 8\u2019th International Workshop on the Mathematical Foundations of Programming Semantics ( 1992 ). Philip Wadler, There\u2019s no substitute for linear logic, 8\u2019th International Workshop on the Mathematical Foundations of Programming Semantics (1992)."},{"key":"e_1_3_2_1_46_1","first-page":"529","volume-title":"Proc. MFPS, LNCS, no. 802","year":"1993","unstructured":", A syntax for linear logic , Proc. MFPS, LNCS, no. 802 , Springer , 1993 , pp. 513\u2013 529 . , A syntax for linear logic, Proc. MFPS, LNCS, no. 802, Springer, 1993, pp. 513\u2013529."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944723"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"},{"key":"e_1_3_2_1_49_1","unstructured":"The logical basis of evaluation order Ph.D. thesis Carnegie Mellon University 2009\n  . The logical basis of evaluation order Ph.D. thesis Carnegie Mellon University 2009."}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837652","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837652","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:38Z","timestamp":1750211018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837652"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":49,"alternative-id":["10.1145\/2837614.2837652","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837652","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837652","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}