{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:10Z","timestamp":1780994710564,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>User-defined effects and effect handlers are advertised and advocated as a relatively easy-to-understand and modular approach to delimited control. They offer the ability of suspending and resuming a computation and allow information to be transmitted both ways between the computation, which requests a certain service, and the handler, which provides this service. Yet, a key question remains, to this day, largely unanswered: how does one modularly specify and verify programs in the presence of both user-defined effect handlers and primitive effects, such as heap-allocated mutable state? We answer this question by presenting a Separation Logic with built-in support for effect handlers, both shallow and deep. The specification of a program fragment includes a protocol that describes the effects that the program may perform as well as the replies that it can expect to receive. The logic allows local reasoning via a frame rule and a bind rule. It is based on Iris and inherits all of its advanced features, including support for higher-order functions, user-defined ghost state, and invariants. We illustrate its power via several case studies, including (1) a generic formulation of control inversion, which turns a producer that ``pushes'' elements towards a consumer into a producer from which one can ``pull'' elements on demand, and (2) a simple system for cooperative concurrency, where several threads execute concurrently, can spawn new threads, and communicate via promises.<\/jats:p>","DOI":"10.1145\/3434314","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["A separation logic for effect handlers"],"prefix":"10.1145","volume":"5","author":[{"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_2_1","unstructured":"Andrej Bauer and Matija Pretnar. 2020. Ef. http:\/\/www.ef-lang.org\/  Andrej Bauer and Matija Pretnar. 2020. Ef. http:\/\/www.ef-lang.org\/"},{"key":"e_1_2_1_3_1","volume-title":"Fundamentals of Software Engineering (Lecture Notes in Computer Science","author":"Berger Martin"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the ACM on Programming Languages 3, POPL ( 2019 ), 6 : 1-6 : 28","author":"Biernacki Dariusz","year":"2019"},{"key":"e_1_2_1_5_1","volume-title":"Efekt: Capability-passing style for type-and efect-safe, extensible efect handlers in Scala. Journal of Functional Programming 30 ( 2020 ), e8","author":"Brachth\u00e4user Jonathan Immanuel","year":"2020"},{"key":"e_1_2_1_6_1","volume-title":"International Conference on Functional Programming (ICFP). 133-144","author":"Brady Edwin C.","year":"2013"},{"key":"e_1_2_1_7_1","volume-title":"Trends in Functional Programming (TFP) (Lecture Notes in Computer Science","author":"Brady Edwin C."},{"key":"e_1_2_1_8_1","article-title":"Deriving a Floyd-Hoare logic for non-local jumps from a formulaeas-types notion of control","volume":"81","author":"Crolard Tristan","year":"2012","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Paulo Em\u00edlio de Vilhena. 2020. A Separation Logic for Efect Handlers: Coq formalization. https:\/\/gitlab.inria.fr\/pdevilhe\/ hazel.  Paulo Em\u00edlio de Vilhena. 2020. A Separation Logic for Efect Handlers: Coq formalization. https:\/\/gitlab.inria.fr\/pdevilhe\/ hazel.","DOI":"10.1145\/3410260"},{"key":"e_1_2_1_10_1","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020a. Control inversion in Multicore OCaml. https:\/\/gitlab.inria.fr\/pdevilhe\/ hazel\/-\/blob\/master\/src\/invert.ml.  Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020a. Control inversion in Multicore OCaml. https:\/\/gitlab.inria.fr\/pdevilhe\/ hazel\/-\/blob\/master\/src\/invert.ml."},{"key":"e_1_2_1_11_1","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020b. Cooperative concurrency in Multicore OCaml. https:\/\/gitlab.inria.fr\/ pdevilhe\/hazel\/-\/blob\/master\/src\/promises.ml.  Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020b. Cooperative concurrency in Multicore OCaml. https:\/\/gitlab.inria.fr\/ pdevilhe\/hazel\/-\/blob\/master\/src\/promises.ml."},{"key":"e_1_2_1_12_1","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020c. Problems with multi-shot continuations in Multicore OCaml. https: \/\/gitlab.inria.fr\/pdevilhe\/hazel\/-\/blob\/master\/src\/test.ml.  Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2020c. Problems with multi-shot continuations in Multicore OCaml. https: \/\/gitlab.inria.fr\/pdevilhe\/hazel\/-\/blob\/master\/src\/test.ml."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500593"},{"key":"e_1_2_1_14_1","volume-title":"Trends in Functional Programming (TFP) (Lecture Notes in Computer Science","author":"Dolan Stephen"},{"key":"e_1_2_1_15_1","unstructured":"Stephan Dolan Anil Madhavapeddy and KC Sivaramakrishnan. 2020. Multicore OCaml. https:\/\/github.com\/ocamlmulticore\/ocaml-multicore\/wiki  Stephan Dolan Anil Madhavapeddy and KC Sivaramakrishnan. 2020. Multicore OCaml. https:\/\/github.com\/ocamlmulticore\/ocaml-multicore\/wiki"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_2_1_17_1","volume-title":"NASA Formal Methods (NFM) (Lecture Notes in Computer Science","author":"Filli\u00e2tre Jean-Christophe"},{"key":"e_1_2_1_18_1","first-page":"415","volume-title":"Shallow Efect Handlers. In Asian Symposium on Programming Languages and Systems (APLAS) (Lecture Notes in Computer Science","volume":"11275","author":"Hillerstr\u00f6m Daniel","year":"2018"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley and Robert Atkey. 2020. Efect handlers via generalised continuations. Journal of Functional Programming 30 ( 2020 ) e5. https:\/\/www.dhil.net\/research\/papers\/generalised_continuations-jfp-draft.pdf  Daniel Hillerstr\u00f6m Sam Lindley and Robert Atkey. 2020. Efect handlers via generalised continuations. Journal of Functional Programming 30 ( 2020 ) e5. https:\/\/www.dhil.net\/research\/papers\/generalised_continuations-jfp-draft.pdf","DOI":"10.1017\/S0956796820000040"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 ( 2018 ) e20. https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf  Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 ( 2018 ) e20. https:\/\/people.mpi-sws.org\/~dreyer\/papers\/iris-ground-up\/paper.pdf","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_2_1_23_1","volume-title":"Asynchronous Liquid Separation Types. In European Conference on Object-Oriented Programming (ECOOP). 396-420","author":"Kloos Johannes","year":"2015"},{"key":"e_1_2_1_24_1","volume-title":"Koka: Programming with Row Polymorphic Efect Types. In Workshop on Mathematically Structured Functional Programming (MSFP)","volume":"153","author":"Leijen Daan","year":"2014"},{"key":"e_1_2_1_25_1","first-page":"16","article-title":"Structured asynchrony with algebraic efects","author":"Leijen Daan","year":"2017","journal-title":"Type-Driven Development (TyDe)."},{"key":"e_1_2_1_26_1","unstructured":"Daan Leijen. 2020. Koka. https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/  Daan Leijen. 2020. Koka. https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/"},{"key":"e_1_2_1_27_1","volume-title":"Formal Methods (FM) (Lecture Notes in Computer Science","author":"Letan Thomas"},{"key":"e_1_2_1_28_1","unstructured":"Sam Lindley Conor McBride and Craig McLaughlin. 2017. Do Be Do Be Do. In Principles of Programming Languages (POPL). http:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/frankly.pdf  Sam Lindley Conor McBride and Craig McLaughlin. 2017. Do Be Do Be Do. In Principles of Programming Languages (POPL). http:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/frankly.pdf"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_2_1_31_1","first-page":"118","article-title":"A Logic for Algebraic Efects","author":"Plotkin Gordon D.","year":"2008","journal-title":"Logic in Computer Science (LICS)."},{"key":"e_1_2_1_32_1","first-page":"80","volume-title":"Handlers of Algebraic Efects. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"5502","author":"Gordon"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018624"},{"key":"e_1_2_1_35_1","first-page":"55","article-title":"Separation Logic","author":"Reynolds John C.","year":"2002","journal-title":"A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the ACM on Programming Languages 4, POPL ( 2020 ), 51 : 1-51 : 32","author":"Zakowski Yannick","year":"2020"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the ACM on Programming Languages 3, POPL ( 2019 ), 5 : 1-5 : 29","author":"Zhang Yizhou"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434314","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434314","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:35Z","timestamp":1750195475000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434314"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434314"],"URL":"https:\/\/doi.org\/10.1145\/3434314","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}