{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:30Z","timestamp":1775790750908,"version":"3.50.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2016\/23\/D\/ST6\/01387, 2018\/31\/D\/ST6\/03951"],"award-info":[{"award-number":["2016\/23\/D\/ST6\/01387, 2018\/31\/D\/ST6\/03951"]}],"id":[{"id":"10.13039\/501100004281","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":[[2020,1]]},"abstract":"<jats:p>\n            Handlers of algebraic effects aspire to be a practical and robust programming construct that allows one to define, use, and combine different computational effects. Interestingly, a critical problem that still bars the way to their popular adoption is how to combine different uses of\n            <jats:italic>the same<\/jats:italic>\n            effect in a program, particularly in a language with a static type-and-effect system. For example, it is rudimentary to define the \u201cmutable memory cell\u201d effect as a pair of operations,\n            <jats:italic>put<\/jats:italic>\n            and\n            <jats:italic>get<\/jats:italic>\n            , together with a handler, but it is far from obvious how to use this effect a number of times to operate a number of memory cells in a single context. In this paper, we propose a solution based on lexically scoped effects in which each use (an \u201cinstance\u201d) of an effect can be singled out by name, bound by an enclosing handler and tracked in the type of the expression. Such a setting proves to be delicate with respect to the choice of semantics, as it depends on the explosive mixture of effects, polymorphism, and reduction under binders. Hence, we devise a novel approach to Kripke-style logical relations that can deal with open terms, which allows us to prove the desired properties of our calculus. We formalise our core results in Coq, and introduce an experimental surface-level programming language to show that our approach is applicable in practice.\n          <\/jats:p>","DOI":"10.1145\/3371116","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Binders by day, labels by night: effect instances via lexically scoped handlers"],"prefix":"10.1145","volume":"4","author":[{"given":"Dariusz","family":"Biernacki","sequence":"first","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}]},{"given":"Maciej","family":"Pir\u00f3g","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}]},{"given":"Piotr","family":"Polesiuk","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}]},{"given":"Filip","family":"Sieczkowski","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004099"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_2_2_12_1","volume-title":"Goodman","author":"Bingham Eli","year":"2018"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237771"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276481"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Lukas Convent Sam Lindley Conor McBride and Craig McLaughlin. 2019. Doo bee doo bee doo. (2019). Draft.  Lukas Convent Sam Lindley Conor McBride and Craig McLaughlin. 2019. Doo bee doo bee doo. (2019). Draft.","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342589"},{"key":"e_1_2_2_20_1","volume-title":"OCaml Users and Developers Workshop","author":"Dolan Stephen","year":"2015"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_17"},{"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"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","volume-title":"The Definition of Standard ML","author":"Milner Robin","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.30"},{"key":"e_1_2_2_39_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034781"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22941-1_13"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_2_2_50_1","volume-title":"Proceedings of the Marktoberdorf Summer School on Program Design Calculi.","author":"Wadler Philip","year":"1992"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371116","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371116"],"URL":"https:\/\/doi.org\/10.1145\/3371116","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}