{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:54Z","timestamp":1775873514354,"version":"3.50.1"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Effect handlers form a powerful construct that can express complex programming abstractions. They are a generalisation of exception handlers, but allow resumption of the continuation from where the effect was raised. Allowing continuations to be resumed at most once (\n                    <jats:italic toggle=\"yes\">one-shot<\/jats:italic>\n                    ) or an arbitrary number of times (\n                    <jats:italic toggle=\"yes\">multi-shot<\/jats:italic>\n                    ) has far-reaching consequences. In addition to performance considerations, multi-shot effects break key rules of reasoning and thus render certain standard transformation\/optimisations unsound, especially in languages with mutable references (such as OCaml 5). It is therefore desirable to statically track whether continuations are used in a one-shot or multi-shot discipline, so that a compiler could use this information to efficiently implement effect handlers and to determine what optimizations it may perform.\n                  <\/jats:p>\n                  <jats:p>\n                    We address this problem by developing a type and effect system\u2013called\n                    <jats:bold>Affect<\/jats:bold>\n                    \u2013which uses affine types to track the usage of continuations. A challenge is to soundly deal with advanced programming features\u2014such as references that store continuations and nested continuations\u2014which are crucial to support challenging examples from the effects literature (such as\n                    <jats:italic toggle=\"yes\">control inversion<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">cooperative concurrency<\/jats:italic>\n                    ). Another challenge is to support generic type signatures of polymorphic effectful functions. We address these challenges by using and extending\n                    <jats:monospace>Rust's Cell<\/jats:monospace>\n                    type and Wadler's\n                    <jats:italic toggle=\"yes\">use types<\/jats:italic>\n                    . To prove soundness of Affect we model types and judgements semantically via a logical relation in the Iris separation logic framework in Coq.\n                  <\/jats:p>","DOI":"10.1145\/3704841","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"126-154","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Affect: An Affine Type and Effect System"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-7780-4772","authenticated-orcid":false,"given":"Orpheas","family":"van Rooij","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"},{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In ESOP (LNCS Vol. 3924). 69\u201383. https:\/\/doi.org\/10.1007\/11693024_6 10.1007\/11693024_6","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Amal J. Ahmed Matthew Fluet and Greg Morrisett. 2005. A step-indexed model of substructural state. In ICFP. 78\u201391. https:\/\/doi.org\/10.1145\/1086365.1086376 10.1145\/1086365.1086376","DOI":"10.1145\/1086365.1086376"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and Amy P. Felty. 2000. A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. In POPL. 243\u2013253. https:\/\/doi.org\/10.1145\/325694.325727 10.1145\/325694.325727","DOI":"10.1145\/325694.325727"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23 5 (2001) 657\u2013683. https:\/\/doi.org\/10.1145\/504709.504712 10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In POPL. 109\u2013122. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In LICS. 56\u201365. https:\/\/doi.org\/10.1145\/3209108.3209189 10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_8_2","unstructured":"Henk P. Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics Vol. 103. North-Holland."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Andrej Bauer and Matija Pretnar. 2014. An Effect System for Algebraic Effects and Handlers. LMCS 10 4 (2014). https:\/\/doi.org\/10.2168\/LMCS-10 10.2168\/LMCS-10(4:9)2014","DOI":"10.2168\/LMCS-10"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. JLAMP 84 1 (2015) 108\u2013123. https:\/\/doi.org\/10.1016\/J.JLAMP.2014.02.001 10.1016\/J.JLAMP.2014.02.001","DOI":"10.1016\/J.JLAMP.2014.02.001"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Nick Benton and Andrew Kennedy. 2001. Exceptional Syntax Journal of Functional Programming. JFP 11 4 (2001) 395\u2013410. https:\/\/doi.org\/10.1017\/S0956796801004099 10.1017\/S0956796801004099","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"Jean-Philippe Bernardy Mathieu Boespflug Ryan R. Newton Simon Peyton Jones and Arnaud Spiwack. 2018. Linear Haskell: Practical linearity in a higher-order polymorphic language. PACMPL 2 POPL (2018) 5:1\u20135:29. https:\/\/doi.org\/10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Dariusz Biernacki Maciej Pir\u00f3g Piotr Polesiuk and Filip Sieczkowski. 2018. Handle with care: relational interpretation of algebraic effects and handlers. PACMPL 2 POPL (2018) 8:1\u20138:30. https:\/\/doi.org\/10.1145\/3158096 10.1145\/3158096","DOI":"10.1145\/3158096"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Jonathan Immanuel Brachth\u00e4user Philipp Schuster and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. PACMPL 4 OOPSLA (2020) 126:1\u2013126:30. https:\/\/doi.org\/10.1145\/3428194 10.1145\/3428194","DOI":"10.1145\/3428194"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Lukas Convent Sam Lindley Conor McBride and Craig McLaughlin. 2020. Doo bee doo bee doo. JFP 30 (2020) e9. https:\/\/doi.org\/10.1017\/S0956796820000039 10.1017\/S0956796820000039","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_3_2_16_2","unstructured":"Paulo Em\u00edlio de Vilhena. 2022. Proof of Programs with Effect Handlers. Ph. D. Dissertation. Universit\u00e9 Paris Cit\u00e9. https:\/\/inria.hal.science\/tel-03891381"},{"key":"e_1_3_2_17_2","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020. Hazel. https:\/\/gitlab.inria.fr\/cambium\/hazel\/."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2021. A separation logic for effect handlers. PACMPL 5 POPL (2021) 1\u201328. https:\/\/doi.org\/10.1145\/3434314 10.1145\/3434314","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2023. A Type System for Effect Handlers and Dynamic Labels. In ESOP (LNCS Vol. 13990). 225\u2013252. https:\/\/doi.org\/10.1007\/978-3-031-30044-8_9 10.1007\/978-3-031-30044-8_9","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Stephen Dolan Spiros Eliopoulos Daniel Hillerstr\u00f6m Anil Madhavapeddy K. C. Sivaramakrishnan and Leo White. 2017. Concurrent System Programming with Effect Handlers. In TFP (LNCS Vol. 10788). 98\u2013117. https:\/\/doi.org\/10.1007\/978-3-319-89719-6_6 10.1007\/978-3-319-89719-6_6","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Amal Ahmed and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7 2 (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:16)2011 10.2168\/LMCS-7(2:16)2011","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Robert Harper. 2016. Practical foundations for programming languages. Cambridge University Press.","DOI":"10.1017\/CBO9781316576892"},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe@ICFP. 15\u201327. https:\/\/doi.org\/10.1145\/2976022.2976033","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2018. Shallow Effect Handlers. In APLAS (LNCS Vol. 11275). 415\u2013435. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_22","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley Robert Atkey and K. C. Sivaramakrishnan. 2017. Continuation Passing Style for Effect Handlers. In FSCD (LIPIcs Vol. 84). 18:1\u201318:19. https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2017.18 10.4230\/LIPICS.FSCD.2017.18","DOI":"10.4230\/LIPICS.FSCD.2017.18"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley and John Longley. 2020. Effects for efficiency: asymptotic speedup with first-class control. PACMPL 4 ICFP (2020) 100:1\u2013100:29. https:\/\/doi.org\/10.1145\/3408982 10.1145\/3408982","DOI":"10.1145\/3408982"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley and John Longley. 2024. Asymptotic speedup via effect handlers. JFP 34 (2024). https:\/\/doi.org\/10.1017\/S0956796824000030 10.1017\/S0956796824000030","DOI":"10.1017\/S0956796824000030"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. 178\u2013198. https:\/\/doi.org\/10.1145\/3437992.3439914 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018. RustBelt: securing the foundations of the Rust programming language. PACMPL 2 POPL (2018) 66:1\u201366:34. https:\/\/doi.org\/10.1145\/3158154 10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256\u2013269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP 28 (2018) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Ohad Kammar Sam Lindley and Nicolas Oury. 2013. Handlers in action. In ICFP. 145\u2013158. https:\/\/doi.org\/10.1145\/2500365.2500590 10.1145\/2500365.2500590","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP (2018) 77:1\u201377:30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS Vol. 10201). 696\u2013723. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_37_2","unstructured":"Daan Leijen. 2005. Extensible records with scoped labels. In TFP Vol. 6. 179\u2013194."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In MSFP@ETAPS (EPTCS Vol. 153). 100\u2013126. https:\/\/doi.org\/10.4204\/EPTCS.153.8 10.4204\/EPTCS.153.8","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In POPL. 486\u2013499. https:\/\/doi.org\/10.1145\/3009837.3009872 10.1145\/3009837.3009872","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Karl Mazurak Jianzhou Zhao and Steve Zdancewic. 2010. Lightweight linear types in system F\u25e6. In TLDI. 77\u201388. https:\/\/doi.org\/10.1145\/1708016.1708027 10.1145\/1708016.1708027","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn John C. Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL (LNCS Vol. 2142). 1\u201319. https:\/\/doi.org\/10.1007\/3-540-44802-0_1 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_42_2","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT press."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In FoSSaCS (LNCS Vol. 2030). 1\u201324. https:\/\/doi.org\/10.1007\/3-540-45315-6_1 10.1007\/3-540-45315-6_1","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Gordon D. Plotkin and John Power. 2002. Notions of Computation Determine Monads. In FoSSaCS (LNCS Vol. 2303). 342\u2013356. https:\/\/doi.org\/10.1007\/3-540-45931-6_24 10.1007\/3-540-45931-6_24","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In ESOP (LNCS Vol. 5502). 80\u201394. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. In MFPS (ENTCS Vol. 319). 19\u201335. https:\/\/doi.org\/10.1016\/J.ENTCS.2015.12.003 10.1016\/J.ENTCS.2015.12.003","DOI":"10.1016\/J.ENTCS.2015.12.003"},{"key":"e_1_3_2_47_2","unstructured":"Didier R\u00e9my. 1994. Type inference for records in natural extension of ML. In Theoretical aspects of object-oriented programming: types semantics and language design. MIT Press 67\u201395."},{"key":"e_1_3_2_48_2","unstructured":"Rust Team. 2024. Module std::cell of the Rust standard library. https:\/\/doc.rust-lang.org\/std\/cell\/."},{"key":"e_1_3_2_49_2","unstructured":"K.C. Sivaramakrishnan. 2015. Pearls of Algebraic Effects and Handlers. https:\/\/kcsrk.info\/ocaml\/multicore\/effects\/2015\/05\/27\/more-effects."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"K. C. Sivaramakrishnan Stephen Dolan Leo White Tom Kelly Sadiq Jaffer and Anil Madhavapeddy. 2021. Retrofitting effect handlers onto OCaml. In PLDI. 206\u2013221. https:\/\/doi.org\/10.1145\/3453483.3454039 10.1145\/3453483.3454039","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In ESOP (LNCS Vol. 8410). 149\u2013168. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Wenhao Tang Daniel Hillerstr\u00f6m Sam Lindley and J. Garrett Morris. 2024. Soundly Handling Linearity. PACMPL 8 POPL (2024) 1600\u20131628. https:\/\/doi.org\/10.1145\/3632896 10.1145\/3632896","DOI":"10.1145\/3632896"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Amin Timany and Lars Birkedal. 2019. Mechanized relational verification of concurrent programs with continuations. PACMPL 3 ICFP (2019) 105:1\u2013105:28. https:\/\/doi.org\/10.1145\/3341709 10.1145\/3341709","DOI":"10.1145\/3341709"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. JACM 71 6 (2024). https:\/\/doi.org\/10.1145\/3676954 10.1145\/3676954","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Jesse A. Tov and Riccardo Pucella. 2011. Practical affine types. In POPL. 447\u2013458. https:\/\/doi.org\/10.1145\/1926385.1926436 10.1145\/1926385.1926436","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","unstructured":"Jesse A. Tov and Riccardo Pucella. 2011. A theory of substructural types and control. In OOPSLA. 625\u2013642. https:\/\/doi.org\/10.1145\/2048066.2048115","DOI":"10.1145\/2048066.2048115"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","unstructured":"Orpheas van Rooij and Robbert Krebbers. 2024. Coq mechanisation of \u201cAffect: An Affine Type and Effect System\u201d. https:\/\/doi.org\/10.5281\/zenodo.14198790 10.5281\/zenodo.14198790","DOI":"10.5281\/zenodo.14198790"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Philip Wadler. 1991. Is There a Use for Linear Logic?. In PEPM. 255\u2013273. https:\/\/doi.org\/10.1145\/115865.115894 10.1145\/115865.115894","DOI":"10.1145\/115865.115894"},{"key":"e_1_3_2_59_2","doi-asserted-by":"crossref","unstructured":"David Walker. 2004. Substructural Type Systems. In Advanced topics in types and programming languages Benjamin C. Pierce (Ed.). MIT press Chapter 1 3\u201343.","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"e_1_3_2_60_2","doi-asserted-by":"crossref","unstructured":"Andrew K. Wright. 1995. Simple Imperative Polymorphism. LISP Symb. Comput. 8 4 (1995) 343\u2013355.","DOI":"10.1007\/BF01018828"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. I&C 115 1 (1994) 38\u201394. https:\/\/doi.org\/10.1006\/INCO.1994.1093 10.1006\/INCO.1994.1093","DOI":"10.1006\/INCO.1994.1093"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Ningning Xie Jonathan Immanuel Brachth\u00e4user Daniel Hillerstr\u00f6m Philipp Schuster and Daan Leijen. 2020. Effect handlers evidently. PACMPL 4 ICFP (2020) 99:1\u201399:29. https:\/\/doi.org\/10.1145\/3408981 10.1145\/3408981","DOI":"10.1145\/3408981"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","unstructured":"Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-safe effect handlers via tunneling. PACMPL 3 POPL (2019) 5:1\u20135:29. https:\/\/doi.org\/10.1145\/3290318 10.1145\/3290318","DOI":"10.1145\/3290318"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704841","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704841","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:37Z","timestamp":1770200077000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704841"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704841"],"URL":"https:\/\/doi.org\/10.1145\/3704841","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}