{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:50Z","timestamp":1780994570664,"version":"3.54.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031300431","type":"print"},{"value":"9783031300448","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider a simple yet expressive <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mi>\u03bb<\/mml:mi>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus equipped with references, effect handlers, and dynamic allocation of effect labels, and whose operational semantics does not involve coercions or rely on type information. We equip this language with a type system that supports type and effect polymorphism, allows reordering row entries and extending a row with new entries, and supports (but is not restricted to) lexically scoped handlers. This requires addressing the issue of potential aliasing between effect names. Our original solution is to interpret a\u00a0row not only as a permission to perform certain effects but also as a disjointness requirement bearing on effect names. The type system guarantees strong type soundness: a\u00a0well-typed program cannot crash or perform an unhandled effect. We prove this fact by encoding the type system into a novel Separation Logic for effect handlers, which we build on top of Iris. Our results are formalized in Coq.<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_9","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"225-252","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["A Type System for Effect Handlers and Dynamic Labels"],"prefix":"10.1007","author":[{"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A.J., Fluet, M., Morrisett, G.: A step-indexed model of substructural state. In: International Conference on Functional Programming (ICFP). pp. 78\u201391 (Sep 2005)","DOI":"10.1145\/1090189.1086376"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pretnar, M.: An effect system for algebraic effects and handlers. Logical Methods in Computer Science 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming 84(1), 108\u2013123 (2015)","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Pir\u00f3g, M., Polesiuk, P., Sieczkowski, F.: Handle with care: relational interpretation of algebraic effects and handlers. Proceedings of the ACM on Programming Languages 2(POPL), 8:1\u20138:30 (2018)","DOI":"10.1145\/3158096"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Pir\u00f3g, M., Polesiuk, P., Sieczkowski, F.: Abstracting algebraic effects. Proceedings of the ACM on Programming Languages 3(POPL), 6:1\u20136:28 (2019)","DOI":"10.1145\/3290319"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Pir\u00f3g, M., Polesiuk, P., Sieczkowski, F.: Binders by day, labels by night: effect instances via lexically scoped handlers. Proceedings of the ACM on Programming Languages 4(POPL), 48:1\u201348:29 (2020)","DOI":"10.1145\/3371116"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Brachth\u00e4user, J.I., Schuster, P., Ostermann, K.: Effects as capabilities: effect handlers and lightweight effect polymorphism. Proceedings of the ACM on Programming Languages 4(OOPSLA), 126:1\u2013126:30 (2020)","DOI":"10.1145\/3428194"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Brachth\u00e4user, J.I., Schuster, P., Ostermann, K.: Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala. Journal of Functional Programming 30, e8 (2020)","DOI":"10.1017\/S0956796820000027"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cooper, E., Lindley, S., Wadler, P., Yallop, J.: Links: Web programming without tiers. In: Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol.\u00a04709, pp. 266\u2013296. Springer (Nov 2006)","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"9_CR10","unstructured":"Dolan, S., White, L.: Syntax with shifted names (Aug 2019), presented at the Workshop on Type-driven Development (TyDe)"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Flatt, M., Yu, G., Findler, R.B., Felleisen, M.: Adding delimited and composable control to a production programming environment. In: International Conference on Functional Programming (ICFP). pp. 165\u2013176 (Oct 2007)","DOI":"10.1145\/1291220.1291178"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Garrigue, J.: Relaxing the value restriction. In: Functional and Logic Programming. Lecture Notes in Computer Science, vol.\u00a02998, pp. 196\u2013213. Springer (Apr 2004)","DOI":"10.1007\/978-3-540-24754-8_15"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hendriks, D., van Oostrom, V.: adbmal. In: International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol.\u00a02741, pp. 136\u2013150. Springer (Aug 2003)","DOI":"10.1007\/978-3-540-45085-6_11"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Hillerstr\u00f6m, D., Lindley, S.: Liberating effects with rows and handlers. In: International Workshop on Type-Driven Development (TyDe@ICFP). pp. 15\u201327 (Sep 2016)","DOI":"10.1145\/2976022.2976033"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hillerstr\u00f6m, D., Lindley, S.: Shallow effect handlers. In: Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science, vol. 11275, pp. 415\u2013435. Springer (Dec 2018)","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28, e20 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Kammar, O., Lindley, S., Oury, N.: Handlers in action. In: International Conference on Functional Programming (ICFP). pp. 145\u2013158 (Sep 2013)","DOI":"10.1145\/2544174.2500590"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Kammar, O., Pretnar, M.: No value restriction is needed for algebraic effects and handlers. Journal of Functional Programming 27, e7 (2017)","DOI":"10.1017\/S0956796816000320"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Principles of Programming Languages (POPL) (Jan 2017)","DOI":"10.1145\/3009837.3009855"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Krogh-Jespersen, M., Svendsen, K., Birkedal, L.: A relational model of type-and-effects in higher-order concurrent separation logic. In: Principles of Programming Languages (POPL). pp. 218\u2013231 (Jan 2017)","DOI":"10.1145\/3093333.3009877"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Koka: Programming with row polymorphic effect types. In: Workshop on Mathematically Structured Functional Programming (MSFP). vol.\u00a0153, pp. 100\u2013126 (Apr 2014)","DOI":"10.4204\/EPTCS.153.8"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Leijen, D.: Type directed compilation of row-typed algebraic effects. In: Principles of Programming Languages (POPL). pp. 486\u2013499 (Jan 2017)","DOI":"10.1145\/3093333.3009872"},{"key":"9_CR23","unstructured":"Leijen, D.: Koka. https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/ (2020)"},{"key":"9_CR24","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml system: documentation and user\u2019s manual (Sep 2019)"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML \u2013 Revised. MIT Press (May 1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Nielsen, L.R.: A selective CPS transformation. Electronic Notes in Theoretical Computer Science 45, 311\u2013331 (Nov 2001)","DOI":"10.1016\/S1571-0661(04)80969-1"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Odersky, M., Boruch-Gruszecki, A., Brachth\u00e4user, J.I., Lee, E., Lhot\u00e1k, O.: Safer exceptions for Scala. In: Symposium on Scala. pp. 1\u201311 (Oct 2021)","DOI":"10.1145\/3486610.3486893"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Pessaux, F., Leroy, X.: Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems 22(2), 340\u2013377 (2000)","DOI":"10.1145\/349214.349230"},{"key":"9_CR29","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press (2002)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Pretnar, M.: Handlers of algebraic effects. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol.\u00a05502, pp. 80\u201394. Springer (Mar 2009)","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"9_CR31","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science (LICS). pp. 55\u201374 (2002)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"R\u00e9my, D.: Type checking records and variants in a natural extension of ML. In: Principles of Programming Languages (POPL). pp. 77\u201388 (1989)","DOI":"10.1145\/75277.75284"},{"key":"9_CR33","unstructured":"The Iris Team: HeapLang. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/-\/blob\/master\/iris_heap_lang\/lang.v (2022)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Tofte, M.: Type inference for polymorphic references. Information and Computation 89(1), 1\u201334 (1990)","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"de\u00a0Vilhena, P.E., Pottier, F.: A separation logic for effect handlers. Proceedings of the ACM on Programming Languages 5(POPL) (Jan 2021)","DOI":"10.1145\/3434314"},{"key":"9_CR36","unstructured":"de\u00a0Vilhena, P.E., Pottier, F.: A type system for effect handlers and dynamic labels: Coq formalization. https:\/\/gitlab.inria.fr\/pdevilhe\/tes (2022)"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Vindum, S.F., Birkedal, L.: Contextual refinement of the Michael-Scott queue. In: Certified Programs and Proofs (CPP). pp. 76\u201390 (Jan 2021)","DOI":"10.1145\/3437992.3439930"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Wand, M.: Type inference for record concatenation and multiple inheritance. Information and Computation 93(1), 1\u201315 (Jul 1991)","DOI":"10.1016\/0890-5401(91)90050-C"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Wright, A.K.: Simple imperative polymorphism. Lisp and Symbolic Computation 8(4), 343\u2013356 (Dec 1995)","DOI":"10.1007\/BF01018828"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38\u201394 (Nov 1994)","DOI":"10.1006\/inco.1994.1093"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Myers, A.C.: Abstraction-safe effect handlers via tunneling. Proceedings of the ACM on Programming Languages 3(POPL), 5:1\u20135:29 (2019)","DOI":"10.1145\/3290318"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Salvaneschi, G., Beightol, Q., Liskov, B., Myers, A.C.: Accepting blame for safe tunneled exceptions. In: Programming Language Design and Implementation (PLDI). pp. 281\u2013295 (Jun 2016)","DOI":"10.1145\/2980983.2908086"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30044-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:03:50Z","timestamp":1686128630000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}