{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T00:23:03Z","timestamp":1787530983707,"version":"build-2736575974"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"UKRI Future Leaders Fellowship","award":["MR\/T043830\/1"],"award-info":[{"award-number":["MR\/T043830\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We propose a novel approach to soundly combining linear types with multi-shot effect handlers. Linear type systems statically ensure that resources such as file handles and communication channels are used exactly once. Effect handlers provide a rich modular programming abstraction for implementing features ranging from exceptions to concurrency to backtracking. Whereas conventional linear type systems bake in the assumption that continuations are invoked exactly once, effect handlers allow continuations to be discarded (e.g. for exceptions) or invoked more than once (e.g. for backtracking). This mismatch leads to soundness bugs in existing systems such as the programming language\n            <jats:sc>Links<\/jats:sc>\n            , which combines linearity (for session types) with effect handlers. We introduce control-flow linearity as a means to ensure that continuations are used in accordance with the linearity of any resources they capture, ruling out such soundness bugs.\n          <\/jats:p>\n          <jats:p>\n            We formalise the notion of control-flow linearity in a System F-style core calculus\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            equipped with linear types, an effect type system, and effect handlers. We define a linearity-aware semantics in order to formally prove that\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            preserves the integrity of linear values in the sense that no linear value is discarded or duplicated. In order to show that control-flow linearity can be made practical, we adapt\n            <jats:sc>Links<\/jats:sc>\n            based on the design of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , in doing so fixing a long-standing soundness bug.\n          <\/jats:p>\n          <jats:p>\n            Finally, to better expose the potential of control-flow linearity, we define an ML-style core calculus\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">Q<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , based on qualified types, which requires no programmer provided annotations, and instead relies entirely on type inference to infer control-flow linearity. Both linearity and effects are captured by qualified types.\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">Q<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            overcomes a number of practical limitations of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mi>eff<\/mml:mi>\n                  <mml:mo>\u2218<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , supporting abstraction over linearity, linearity dependencies between type variables, and a much more fine-grained notion of control-flow linearity.\n          <\/jats:p>","DOI":"10.1145\/3632896","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1600-1628","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Soundly Handling Linearity"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6589-3821","authenticated-orcid":false,"given":"Wenhao","family":"Tang","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4730-9315","authenticated-orcid":false,"given":"Daniel","family":"Hillerstr\u00f6m","sequence":"additional","affiliation":[{"name":"Huawei Zurich Research Center, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3992-1080","authenticated-orcid":false,"given":"J. Garrett","family":"Morris","sequence":"additional","affiliation":[{"name":"University of Iowa, Iowa, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086376"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_4_1","volume-title":"Dual Intuitionistic Linear Logic","author":"Barber Andrew","year":"1996","unstructured":"Andrew Barber. 1996. Dual Intuitionistic Linear Logic. Technical Report ECS-LFCS-96-347. Laboratory for Foundations of Computer Science, The University of Edinburgh, UK."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/JJLAMP.2014.02.001"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_3_2_10_1","unstructured":"Jonathan Immanuel Brachth\u00e4user and Daan Leijen. 2023. Qualified Effect Types \u2013 Taming Control-Flow through Linear Effect Handlers. Technical Report MSR-TR-2023-42. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/qualified-effect-types\/"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231395"},{"key":"e_1_3_2_14_1","unstructured":"Guillaume Combette and Guillaume Munch-Maccagnoni. 2018. A Resource Modality for RAII. In LOLA 2018: Workshop on Syntax and Semantics of Low-Level Languages. 1\u20134."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_18_1","volume-title":"Algebraic Subtyping","author":"Dolan Stephen","year":"2016","unstructured":"Stephen Dolan. 2016. Algebraic Subtyping. Ph. D. Dissertation. Computer Laboratory, University of Cambridge, United Kingdom."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2851099"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143174"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Yannick Forster Ohad Kammar Sam Lindley and Matija Pretnar. 2019. On the expressive power of user-defined effects: Effect handlers monadic reflection delimited control. J. Funct. Program. 29 (2019) e15. https:\/\/doi.org\/10.1017\/S0956796819000121 10.1017\/S0956796819000121","DOI":"10.1017\/S0956796819000121"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318654"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-46490-4_23"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Edward Gan Jesse A. Tov and Greg Morrisett. 2014. Type Classes for Lightweight Substructural Types. In LINEARITY (EPTCS Vol. 176). 34\u201348. https:\/\/doi.org\/10.4204\/EPTCS.176.4 10.4204\/EPTCS.176.4","DOI":"10.4204\/EPTCS.176.4"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563445"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_2_29_1","unstructured":"James Gosling Bill Joy Guy Steele Gilad Bracha Alex Buckley Daniel Smith and Gavin Bierman. 2023. The Java Language Specification: Java SE 20 Edition. https:\/\/docs.oracle.com\/javase\/specs\/jls\/se20\/html\/index.html. [Accessed 2023-07-11]."},{"key":"e_1_3_2_30_1","volume-title":"Foundations for Programming and Implementing Effect Handlers","author":"Hillerstr\u00f6m Daniel","year":"2022","unstructured":"Daniel Hillerstr\u00f6m. 2022. Foundations for Programming and Implementing Effect Handlers. Ph.D. Dissertation. School of Informatics, The University of Edinburgh, UK."},{"key":"e_1_3_2_31_1","unstructured":"Daniel Hillerstr\u00f6m Daan Leijen Sam Lindley Matija Pretnar Andreas Rossberg and KC Sivamarakrishnan. 2022. WebAssembly Typed Continuations Proposal. https:\/\/github.com\/wasmfx\/specfx\/blob\/main\/proposals\/continuations\/Explainer.md [Accessed 2023-11-14]."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000040"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408982"},{"key":"e_1_3_2_36_1","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley and John Longley. 2023. Asymptotic Speedup with Effect Handlers. Draft.","DOI":"10.1017\/S0956796824000030"},{"key":"e_1_3_2_37_1","volume-title":"Compilation of Effect Handlers and their Applications in Concurrency","author":"Hillerstr\u00f6m Daniel","year":"2016","unstructured":"Daniel Hillerstr\u00f6m. 2016. Compilation of Effect Handlers and their Applications in Concurrency. Master by Research thesis. School of Informatics, The University of Edinburgh, UK."},{"key":"e_1_3_2_38_1","volume-title":"Compiling Links Effect Handlers to the OCaml Backend","author":"Hillerstr\u00f6m Daniel","year":"2016","unstructured":"Daniel Hillerstr\u00f6m, Sam Lindley, and KC Sivaramakrishnan. 2016. Compiling Links Effect Handlers to the OCaml Backend. ML Workshop."},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00005-0"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000131"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03034-5_17"},{"key":"e_1_3_2_43_1","unstructured":"Daan Leijen. 2005. Extensible records with scoped labels. In Trends in Functional Programming (Trends in Functional Programming Vol. 6). Intellect 179\u2013194."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_3_2_48_1","doi-asserted-by":"crossref","unstructured":"Sam Lindley and J Garrett Morris. 2017. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers (2017) 265\u2013286.","DOI":"10.1201\/9781003337331-12"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951925"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622814"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2019.30"},{"issue":"4","key":"e_1_3_2_56_1","article-title":"Handling Algebraic Effects","volume":"9","author":"Plotkin Gordon D.","year":"2013","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Log. Methods Comput. Sci. 9, 4 (2013).","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_2_57_1","volume-title":"Type inference in the presence of subtyping: from theory to practice","author":"Pottier Fran\u00e7ois","year":"1998","unstructured":"Fran\u00e7ois Pottier. 1998. Type inference in the presence of subtyping: from theory to practice. Ph.D. Dissertation. INRIA."},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2963"},{"key":"e_1_3_2_59_1","unstructured":"Ron Pressler. 2018. Project Loom: Fibers and Continuations for the Java Virtual Machine. https:\/\/cr.openjdk.org\/~rpressler\/loom\/Loom-Proposal.html. Accessed 2023-04-14."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:21)2014"},{"key":"e_1_3_2_61_1","first-page":"67","volume-title":"Theoretical Aspects of Object-oriented Programming","author":"R\u00e9my Didier","year":"1994","unstructured":"Didier R\u00e9my. 1994. Theoretical Aspects of Object-oriented Programming. MIT Press, Cambridge, MA, USA, Chapter Type Inference for Records in Natural Extension of ML, 67\u201395."},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","unstructured":"Wenhao Tang Daniel Hillerstr\u00f6m Sam Lindley and Garrett Morris. 2023. POPL24 Artifact for Soundly Handling Linearity. https:\/\/doi.org\/10.5281\/zenodo.10120126 10.5281\/zenodo.10120126","DOI":"10.5281\/zenodo.10120126"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926436"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048115"},{"key":"e_1_3_2_66_1","doi-asserted-by":"crossref","unstructured":"David Walker. 2005. Substructural type systems. Advanced topics in types and programming languages (2005) 3\u201344.","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563289"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632896","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632896","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:26Z","timestamp":1751659466000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632896"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632896"],"URL":"https:\/\/doi.org\/10.1145\/3632896","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}