{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:43:32Z","timestamp":1770284612883,"version":"3.49.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.<\/jats:p>","DOI":"10.1145\/3408981","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Effect handlers, evidently"],"prefix":"10.1145","volume":"4","author":[{"given":"Ningning","family":"Xie","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Hillerstr\u00f6m","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"Schuster","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daan","family":"Leijen","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, 157-166","author":"Baars Arthur I."},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Andrej Bauer and Matija Pretnar. 2014. An Efect System for Algebraic Efects and Handlers. Logical Methods in Computer Science 10 ( 4 ).  Andrej Bauer and Matija Pretnar. 2014. An Efect System for Algebraic Efects and Handlers. Logical Methods in Computer Science 10 ( 4 ).","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_5_1","volume-title":"Proc. ACM Program. Lang. 2 ( POPL '17 issue): 8 : 1-8 : 30","author":"Biernacki Dariusz","year":"2017"},{"key":"e_1_2_2_6_1","volume-title":"Proc. ACM Program. Lang. 4 ( POPL ). Association for Computing Machinery","author":"Biernacki Dariusz","year":"2019"},{"key":"e_1_2_2_7_1","volume-title":"Efekt: Extensible Algebraic Efects in Scala. In Scala' 17.","author":"Brachth\u00e4user Jonathan Immanuel","year":"2017"},{"key":"e_1_2_2_8_1","volume-title":"Proc. ACM Program. Lang. 2 ( OOPSLA ). Association for Computing Machinery","author":"Brachth\u00e4user Jonathan Immanuel","year":"2018"},{"key":"e_1_2_2_9_1","volume-title":"Efekt: Lightweight Efect Polymorphism for Handlers. Technical Report","author":"Brachth\u00e4user Jonathan Immanuel","year":"2020"},{"key":"e_1_2_2_10_1","volume-title":"Efekt: Capability-Passing Style for Typeand Efect-Safe, Extensible Efect Handlers in Scala. Journal of Functional Programming","author":"Brachth\u00e4user Jonathan Immanuel","year":"2020"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the Symposium on Trends in Functional Programming. TFP'17","author":"Dolan Stephen","year":"2017"},{"key":"e_1_2_2_12_1","volume-title":"OCaml Workshop.","author":"Dolan Stephen","year":"2015"},{"key":"e_1_2_2_13_1","volume-title":"Simon Peyton Jones, and Amr Sabry","author":"Dyvbig R Kent","year":"2007"},{"key":"e_1_2_2_14_1","volume-title":"Monadic Reflection, Delimited Control. Journal of Functional Programming 29","author":"Forster Yannick","year":"1900"},{"key":"e_1_2_2_15_1","volume-title":"Jones","author":"Gaster Ben R.","year":"1996"},{"key":"e_1_2_2_16_1","volume-title":"Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, 12-23. FPCA '95. ACM","author":"Gunter Carl A."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_18_1","first-page":"415","volume-title":"Shallow Efect Handlers. In 16th Asian Symposium on Programming Languages and Systems (APLAS'18)","author":"Hillerstr\u00f6m Daniel","year":"2018"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the Second International Conference on Formal Structures for Computation and Deduction. FSCD'17","author":"Hillerstr\u00f6m Daniel","year":"2017"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_17"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_2_2_22_1","volume-title":"No Value Restriction Is Needed for Algebraic Efects and Handlers. Journal of Functional Programming 27 ( 1 )","author":"Kammar Ohad"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503791"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Oleg Kiselyov and Chung-chieh Shan. 2009. Embedded Probabilistic Programming. In Domain-Specific Languages. doi:10.1007\/978-3-642-03034-5_17.  Oleg Kiselyov and Chung-chieh Shan. 2009. Embedded Probabilistic Programming. In Domain-Specific Languages. doi:10.1007\/978-3-642-03034-5_17.","DOI":"10.1007\/978-3-642-03034-5_17"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159808"},{"key":"e_1_2_2_26_1","volume-title":"Proceedings of the 2005 Symposium on Trends in Functional Programming, 297-312","author":"Leijen Daan","year":"2005"},{"key":"e_1_2_2_27_1","volume-title":"Koka: Programming with Row Polymorphic Efect Types. In MSFP'14","author":"Leijen Daan","year":"2014"},{"key":"e_1_2_2_28_1","first-page":"339","article-title":"Implementing Algebraic Efects in C: Or Monads for Free in C. Edited by Bor-Yuh Evan Chang. Programming Languages and Systems, LNCS, 10695 ( 1 ). Suzhou","author":"Leijen Daan","year":"2017","journal-title":"China"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122977"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_31_1","unstructured":"Daan Leijen. 2019. Koka Repository. https:\/\/github.com\/koka-lang\/koka.  Daan Leijen. 2019. Koka Repository. https:\/\/github.com\/koka-lang\/koka."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"e_1_2_2_35_1","volume-title":"Existential Types: Logical Relations and Operational Equivalence. In In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, 309-326","author":"Pitts Andrew M.","year":"1998"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633360"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_39_1","volume-title":"Logic and Handling of Algebraic Efects. Phdthesis","author":"Pretnar Matija"},{"key":"e_1_2_2_40_1","volume-title":"An Introduction to Algebraic Efects and Handlers. Invited Tutorial Paper. Electron. Notes Theor. Comput. Sci. 319 (C)","author":"Pretnar Matija","year":"2015"},{"key":"e_1_2_2_41_1","volume-title":"Axel Faes, and Tom Schrijvers.","author":"Pretnar Matija","year":"2017"},{"key":"e_1_2_2_42_1","first-page":"67","article-title":"Type Inference for Records in Natural Extension of ML","author":"R\u00e9my Didier","year":"1994","journal-title":"Theoretical Aspects of Object-Oriented Programming"},{"key":"e_1_2_2_43_1","volume-title":"Proceedings of the International Conference on Functional Programming. ACM","author":"Schuster Philipp","year":"2020"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_2_2_47_1","unstructured":"Ningning Xie Jonathan Brachth\u00e4user Daniel Hillerstr\u00f6m Philipp Schuster and Daan Leijen. Jul. 2020. Efect Handlers Evidently. MSR-TR-2020-23. Microsoft Research. Extended version with proofs.  Ningning Xie Jonathan Brachth\u00e4user Daniel Hillerstr\u00f6m Philipp Schuster and Daan Leijen. Jul. 2020. Efect Handlers Evidently. MSR-TR-2020-23. Microsoft Research. Extended version with proofs."},{"key":"e_1_2_2_48_1","volume-title":"Evidently. In Proceedings of the 2020 ACM SIGPLAN Symposium on Haskell. Haskell'20","author":"Xie Ningning","year":"2020"},{"key":"e_1_2_2_49_1","volume-title":"Proc. ACM Program. Lang. 3 (POPL). ACM. doi:10","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\/3408981","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408981","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:58Z","timestamp":1750193278000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408981"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408981"],"URL":"https:\/\/doi.org\/10.1145\/3408981","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}