{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:28Z","timestamp":1780994668259,"version":"3.54.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"name":"UKRI Future Leaders Fellowship","award":["MR\/V024299\/1"],"award-info":[{"award-number":["MR\/V024299\/1"]}]},{"name":"European Research Council","award":["101171349"],"award-info":[{"award-number":["101171349"]}]},{"DOI":"10.13039\/501100003246","name":"Dutch Research Council","doi-asserted-by":"crossref","award":["OCENW.XL.23.089"],"award-info":[{"award-number":["OCENW.XL.23.089"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Effect handlers offer a powerful and relatively simple mechanism for controlling a program's flow of execution. Since their introduction, an impressive array of verification tools for effect handlers has been developed. However, to this day, no framework can express and prove relational properties about programs that use effect handlers in languages such as OCaml and Links, where programming features like mutable state and concurrency are readily available. To this end, we introduce blaze, the first relational separation logic for effect handlers. We build blaze on top of the Rocq implementation of the Iris separation logic, thereby enjoying the rigour of a mechanised theory and all the reasoning properties of a modern fully-fledged concurrent separation logic, such as modular reasoning about stateful concurrent programs and the ability to introduce user-defined ghost state. In addition to familiar reasoning rules, such as the bind rule and the frame rule, blaze offers rules to reason modularly about programs that perform and handle effects. Significantly, when verifying that two programs are related, blaze does not require that effects and handlers from one program be in correspondence with effects and handlers from the other. To assess this flexibility, we conduct a number of case studies: most noticeably, we show how different implementations of an asynchronous-programming library using effects are related to truly concurrent implementations. As side contributions, we introduce two new, simple, and general reasoning rules for concurrent relational separation logic that are independent of effects: a logical-fork rule that allows one to reason about an arbitrary program phrase as if it had been spawned as a thread and a thread-swap rule that allows one to reason about how threads are scheduled.<\/jats:p>","DOI":"10.1145\/3776676","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"981-1009","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Relational Separation Logic for Effect Handlers"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7379-310X","authenticated-orcid":false,"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9621-1415","authenticated-orcid":false,"given":"Simcha","family":"van Collem","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8985-6156","authenticated-orcid":false,"given":"Ines","family":"Wright","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Amal J. Ahmed Andrew W. Appel and Roberto Virga. 2002. A Stratified Semantics of General References Embeddable in Higher-Order Logic. In Logic in Computer Science (LICS). 75\u201386. https:\/\/doi.org\/10.1109\/LICS.2002.1029818 10.1109\/LICS.2002.1029818","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704915"},{"key":"e_1_2_1_3_1","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 Principles of Programming Languages (POPL). 109\u2013122. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_2_1_8_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2012. A note on the transitivity of step-indexed logical relations. Nov. https:\/\/abizjak.github.io\/documents\/notes\/step-indexed-transitivity.pdf"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000027"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462166.1462167"},{"key":"e_1_2_1_14_1","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_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_2_1_17_1","unstructured":"Paulo Em\u00edlio de Vilhena Simcha van Collem Ines Wright and Robbert Krebbers. 2026. A Relational Separation Logic for Effect Handlers \u2013 Rocq Formalisation. https:\/\/github.com\/DeVilhena-Paulo\/blaze"},{"key":"e_1_2_1_18_1","unstructured":"Paulo Em\u00edlio de Vilhena Simcha van Collem Ines Wright and Robbert Krebbers. 2026. A Relational Separation Logic for Effect Handlers \u2013 Technical Appendix. https:\/\/devilhena-paulo.github.io\/files\/blaze.pdf"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2010.09.021"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Logic in Computer Science (LICS). 442\u2013451. https:\/\/doi.org\/10.1145\/3209108.3209174 10.1145\/3209108.3209174","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(3:9)2021"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_1_25_1","unstructured":"Haskell Community. 2023. Alternative and MonadPlus. https:\/\/en.wikibooks.org\/wiki\/Haskell\/Alternative_and_MonadPlus"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_30_1","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 Principles of Programming Languages (POPL). 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Ohad Kammar Paul B. Levy Sean K. Moss and Sam Staton. 2017. A monad for full ground reference cells. In Logic in Computer Science (LICS). https:\/\/doi.org\/10.1109\/LICS.2017.8005109 10.1109\/LICS.2017.8005109","DOI":"10.1109\/LICS.2017.8005109"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Robert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Luko van der Maas and Enrico Tassi. 2025. Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. In Interactive Theorem Proving (ITP). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2025.27 10.4230\/LIPICS.ITP.2025.27","DOI":"10.4230\/LIPICS.ITP.2025.27"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_1_38_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my KC Sivaramakrishnan and J\u00e9r\u00f4me Vouillon. 2025. The OCaml system: Documentation and user\u2019s manual. https:\/\/ocaml.org\/manual\/5.3\/index.html"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Sam Lindley Conor McBride and Craig McLaughlin. 2017. Do Be Do Be Do. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3009837.3009897 10.1145\/3009837.3009897","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.7488\/ERA\/537"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In Logic in Computer Science (LICS). 255\u2013266. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_43_1","volume-title":"Operational reasoning for functions with local state","author":"Pitts Andrew","unstructured":"Andrew Pitts and Ian Stark. 1999. Operational reasoning for functions with local state. Cambridge University Press, 227\u2013274."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.003"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363518"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632896"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720476"},{"key":"e_1_2_1_53_1","unstructured":"The Iris Team. 2025. Iris Fixpoint Operators. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/-\/blob\/master\/iris\/bi\/lib\/fixpoint_mono.v"},{"key":"e_1_2_1_54_1","unstructured":"The Rocq Prover development team. 2025. The Rocq Prover. https:\/\/rocq-prover.org\/"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704841"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In Certified Programs and Proofs (CPP). 76\u201390. https:\/\/doi.org\/10.1145\/3437992.3439930 10.1145\/3437992.3439930","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Simon Friis Vindum Dan Frumin and Lars Birkedal. 2022. Mechanized verification of a fine-grained concurrent queue from Meta\u2019s Folly library. In Certified Programs and Proofs (CPP). 100\u2013115. https:\/\/doi.org\/10.1145\/3497775.3503689 10.1145\/3497775.3503689","DOI":"10.1145\/3497775.3503689"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908086"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776676","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:04:33Z","timestamp":1767899073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776676"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776676"],"URL":"https:\/\/doi.org\/10.1145\/3776676","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}