{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:50:20Z","timestamp":1790927420795,"version":"4.1.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NNX16AB09G"],"award-info":[{"award-number":["NNX16AB09G"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1513797"],"award-info":[{"award-number":["1513797"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Algebraic effect handlers offer a unified approach to expressing control-flow transfer idioms such as exceptions, iteration, and async\/await. Unfortunately, previous attempts to make these handlers type-safe have failed to support the fundamental principle of modular reasoning for higher-order abstractions. We demonstrate that abstraction-safe algebraic effect handlers are possible by giving them a new semantics. The key insight is that code should only handle effects it is aware of. In our approach, the type system guarantees all effects are handled, but it is impossible for higher-order, effect-polymorphic code to accidentally handle effects raised by functions passed in; such effects tunnel through the higher-order, calling procedures polymorphic to them. By contrast, the possibility of accidental handling threatens previous designs for algebraic effect handlers. We prove that our design is not only type-safe, but also abstraction-safe. Using a logical-relations model that we prove sound with respect to contextual equivalence, we derive previously unattainable program equivalence results. Our mechanism offers a viable approach for future language designs aiming for effect handlers with strong abstraction guarantees.<\/jats:p>","DOI":"10.1145\/3290318","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Abstraction-safe effect handlers via tunneling"],"prefix":"10.1145","volume":"3","author":[{"given":"Yizhou","family":"Zhang","sequence":"first","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew C.","family":"Myers","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273922"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136007"},{"key":"e_1_2_2_9_1","volume-title":"Proc. ACM on Programming Languages, 2(OOPSLA)","author":"Brachth\u00e4user Jonathan Immanuel","year":"2018","unstructured":"Jonathan Immanuel Brachth\u00e4user , Philipp Schuster , and Klaus Ostermann . Algebraic effects for the masses . Proc. ACM on Programming Languages, 2(OOPSLA) , October 2018 . Jonathan Immanuel Brachth\u00e4user, Philipp Schuster, and Klaus Ostermann. Algebraic effects for the masses. Proc. ACM on Programming Languages, 2(OOPSLA), October 2018."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236762"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_13_1","volume-title":"Milner award lecture: The type soundness theorem that you really want to prove (and now you can). In 45 th ACM Symp. on Principles of Programming Languages (POPL)","author":"Dreyer Derek","year":"2018","unstructured":"Derek Dreyer . Milner award lecture: The type soundness theorem that you really want to prove (and now you can). In 45 th ACM Symp. on Principles of Programming Languages (POPL) , 2018 . Derek Dreyer. Milner award lecture: The type soundness theorem that you really want to prove (and now you can). In 45 th ACM Symp. on Principles of Programming Languages (POPL), 2018."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006259"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_2_19_1","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"Gamma Erich","year":"1994","unstructured":"Erich Gamma , Richard Helm , Ralph Johnson , and John Vlissides . Design Patterns: Elements of Reusable Object-Oriented Software . Addison Wesley , Reading, MA , 1994 . ISBN 0-201-63361-2. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, Reading, MA, 1994. ISBN 0-201-63361-2."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_2_2_25_1","volume-title":"The TEXbook","author":"Knuth Donald Ervin","year":"1984","unstructured":"Donald Ervin Knuth . The TEXbook . Addison-Wesley Reading , 1984 . Donald Ervin Knuth. The TEXbook. Addison-Wesley Reading, 1984."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325708"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_31_1","volume-title":"The Definition of Standard ML","author":"Milner Robin","year":"1990","unstructured":"Robin Milner , Mads Tofte , and Robert Harper . The Definition of Standard ML . MIT Press , Cambridge, MA , 1990 . ISBN 978-0262631327. Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, MA, 1990. ISBN 978-0262631327."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158130"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869489"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_2_36_1","first-page":"273","volume-title":"Operational reasoning for functions with local state. Higher order operational techniques in semantics","author":"Pitts Andrew M","year":"1998","unstructured":"Andrew M Pitts and Ian Stark . Operational reasoning for functions with local state. Higher order operational techniques in semantics , pages 227\u2013 273 , 1998 . Andrew M Pitts and Ian Stark. Operational reasoning for functions with local state. Higher order operational techniques in semantics, pages 227\u2013273, 1998."},{"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":"IxFree: Step-indexed logical relations in Coq. In 3 rd International Workshop on Coq for Programming Languages (CoqPL)","author":"Polesiuk Piotr","year":"2017","unstructured":"Piotr Polesiuk . IxFree: Step-indexed logical relations in Coq. In 3 rd International Workshop on Coq for Programming Languages (CoqPL) , 2017 . Piotr Polesiuk. IxFree: Step-indexed logical relations in Coq. In 3 rd International Workshop on Coq for Programming Languages (CoqPL), 2017."},{"key":"e_1_2_2_40_1","first-page":"523","volume-title":"IFIP Congress","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . Types, abstraction and parametric polymorphism . In IFIP Congress , pages 513\u2013 523 , 1983 . John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513\u2013523, 1983."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/95411"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_47_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\/10.1145\/3290318","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290318","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290318"],"URL":"https:\/\/doi.org\/10.1145\/3290318","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}