{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:12Z","timestamp":1784211252487,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2023-04632"],"award-info":[{"award-number":["RGPIN-2023-04632"]}],"id":[{"id":"10.13039\/501100000038","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":[[2026,1,8]]},"abstract":"<jats:p>\n                    Metaprogramming and effect handlers interact in unexpected, and sometimes undesirable, ways. One example is scope extrusion: the generation of ill-scoped code. Scope extrusion can either be preemptively prevented, via static type systems, or retroactively detected, via dynamic checks. Static type systems exist in theory, but struggle with a range of implementation and usability problems in practice. In contrast, dynamic checks exist in practice (e.g. in MetaOCaml), but are understudied in theory. Designers of metaprogramming languages are thus given little guidance regarding the design and implementation of checks. We present the first formal study of dynamic scope extrusion checks, introducing a calculus (\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi>\u03bb<\/mml:mi>\n                          <mml:mrow>\n                            <mml:mo fence=\"false\" stretchy=\"false\">\u27e8<\/mml:mo>\n                            <mml:mo fence=\"false\" stretchy=\"false\">\u27e8<\/mml:mo>\n                            <mml:mi>o<\/mml:mi>\n                            <mml:mi>p<\/mml:mi>\n                            <mml:mo fence=\"false\" stretchy=\"false\">\u27e9<\/mml:mo>\n                            <mml:mo fence=\"false\" stretchy=\"false\">\u27e9<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:msub>\n                      <\/mml:math>\n                      )\n                    <\/jats:inline-formula>\n                    for describing and evaluating checks. Further, we introduce a novel dynamic check - the \"Cause-for-Concern\" check - which we prove correct, characterise without reference to its implementation, and argue combines the advantages of existing dynamic checks. Finally, we extend our framework with refined environment classifiers, which statically prevent scope extrusion, and compare their expressivity with the dynamic checks.\n                  <\/jats:p>","DOI":"10.1145\/3776681","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1123-1152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-3018-4389","authenticated-orcid":false,"given":"Michael","family":"Lee","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5961-1493","authenticated-orcid":false,"given":"Ningning","family":"Xie","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2570-2186","authenticated-orcid":false,"given":"Oleg","family":"Kiselyov","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1650-6340","authenticated-orcid":false,"given":"Jeremy","family":"Yallop","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-10(4:9)2014"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Dariusz Biernacki Maciej Pir\u00f3g Piotr Polesiuk and Filip Sieczkowski. 2017. Handle with care: relational interpretation of algebraic effects and handlers. Proc. ACM Program. Lang. 2 POPL Article 8 (Dec. 2017) 30 pages. doi:10.1145\/3158096","DOI":"10.1145\/3158096"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45022-X_4"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39815-8_4"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Jacques Carette Mustafa Elsheikh and W. Spencer Smith. 2011. A generative geometric kernel. In Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation PEPM 2011 Austin TX USA January 24-25 2011 Siau-Cheng Khoo and Jeremy G. Siek (Eds.). ACM 53-62. doi:10.1145\/1929501.1929510","DOI":"10.1145\/1929501.1929510"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Tsung-Ju Chiang Jeremy Yallop Leo White and Ningning Xie. 2024. Staged Compilation with Module Functors. Proc. ACM Program. Lang. 8 ICFP Article 260 (Aug. 2024) 35 pages. doi:10.1145\/3674649","DOI":"10.1145\/3674649"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Matthias Felleisen Mitchell Wand Daniel P. Friedman and Bruce F. Duba. 1988. Abstract Continuations: A Mathematical Semantics for Handling Full Jumps. In Proceedings of the 1988 ACM Conference on LISP and Functional Programming LFP 1988 Snowbird Utah USA July 25-27 1988 J\u00e9r\u00f4me Chailloux (Ed.). ACM 52-62. doi:10.1145\/62678.62684","DOI":"10.1145\/62678.62684"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Matthew Flatt and R. Kent Dybvig. 2020. Compiler and runtime support.for continuation marks. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation PLDI 2020 London UK June 15-20 2020 Alastair F. Donaldson and Emina Torlak.(Eds.). ACM 45-58. doi:10.1145\/3385412.3385981","DOI":"10.1145\/3385412.3385981"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_18"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Kanaru Isoda Ayato Yokoyama and Yukiyoshi Kameyama. 2024. Type-Safe Code Generation with Algebraic Effects and Handlers. In Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (Pasadena CA USA) (GPCE '24). Association for Computing Machinery New York NY USA 53-65. doi:10.1145\/3689484.3690731","DOI":"10.1145\/3689484.3690731"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.08.007"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000256"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.025"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_6"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.103015"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-97-2300-3_12"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Oleg Kiselyov Aggelos Biboudis Nick Palladinos and Yannis Smaragdakis. 2017. Stream fusion to completeness. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017 Paris France January 18-20 2017 Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM 285-299. doi:10.1145\/3009837.3009880","DOI":"10.1145\/3009837.3009880"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_15"},{"key":"e_1_3_2_21_1","unstructured":"Wiktor Kuchta. 2023. A proof of normalization for effect handlers. https:\/\/icfp23.sigplan.org\/details\/hope-2023\/4\/A-proof-of-normalization-for-effect-handlers Seattle Washington United States."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/182590.182483"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Michael Lee Ningning Xie Oleg Kiselyov and Jeremy Yallop. 2025. Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks (Artifact). Zenodo (Nov. 2025). doi:10.5281\/zenodo.17273738","DOI":"10.5281\/zenodo.17273738"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Yannis Lilis and Anthony Savidis. 2019. A Survey of Metaprogramming Languages. ACM Comput. Surv. 52 6 Article 113 (Oct. 2019) 39 pages. doi:10.1145\/3354584","DOI":"10.1145\/3354584"},{"issue":"3","key":"e_1_3_2_26_1","first-page":"23:1","article-title":"Contextual Modal Type Theory","volume":"9","author":"Nanevski Aleksandar","year":"2008","unstructured":"Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual Modal Type Theory. Transactions on Computational Logic 9, 3 (June 2008), 23:1-49.","journal-title":"Transactions on Computational Logic"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Georg Ofenbeck Tiark Rompf and Markus P\u00fcschel. 2016. RandIR: differential testing for embedded compilers. In Proceedings of the 7th ACM SIGPLAN Symposium on Scala SCALA@SPLASH 2016 (Amsterdam Netherlands) Aggelos Biboudis Manohar Jonnalagedda Sandro Stucki and Vlad Ureche.(Eds.). ACM 21-30. doi:10.1145\/2998392","DOI":"10.1145\/2998392"},{"key":"e_1_3_2_28_1","unstructured":"Lionel Emile Vincent Parreaux. 2020. Type-Safe Metaprogramming and Compilation Techniques. For Designing Efficient Systems in High-Level Languages. Ph. D. Dissertation. EPFL."},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Gordon Plotkin and Ningning Xie. 2025. Handling the Selection Monad. Proc. ACM Program. Lang. 9 PLDI (2025). doi:10.1145\/3729321","DOI":"10.1145\/3729321"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784760"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Gabriel Scherer. 2017. Deciding equivalence with sums and the empty.type. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris France) (POPL '17). Association for Computing Machinery New York NY USA 374-386. doi:10.1145\/3009837.3009901","DOI":"10.1145\/3009837.3009901"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Tim Sheard and Simon Peyton. Jones. 2002. Template meta-programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Pittsburgh Pennsylvania) (Haskell '02). Association for Computing Machinery New York NY USA 1-16. doi:10.1145\/581690.581691","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"KC Sivaramakrishnan Stephen Dolan Leo White Tom Kelly Sadiq Jaffer and Anil Madhavapeddy. 2021. Retrofitting effect handlers onto OCaml. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual Canada) (PLDI 2021). Association for Computing Machinery New York NY USA 206-221. doi:10.1145\/3453483.3454039","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Nicolas Stucki Aggelos Biboudis and Martin Odersky. 2018. A practical unification of multi-stage programming and macros. In Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences GPCE 2018 Boston MA USA November 5-6 2018 Eric Vaan Wyk and Tiark Rompf.(Eds.). ACM 14-27. doi:10.1145\/3278122.3278139","DOI":"10.1145\/3278122.3278139"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012984529382"},{"key":"e_1_3_2_37_1","doi-asserted-by":"crossref","unstructured":"Kedar Swadi Walid Taha Oleg Kiselyov and Emir Pa\u0161ali\u0107. 2006. A Monadic Approach for Avoiding Code Duplication When Staging Memoized Functions. In PEPM (Charleston SC). 160-169.","DOI":"10.1145\/1111542.1111570"},{"key":"e_1_3_2_38_1","unstructured":"Walid Taha. 1999. Multi-Stage Programming: Its Theory and Applications. Ph. D. Dissertation. Halmstad University Sweden. https:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:hh:diva-15052"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Walid Taha and Michael Florentin Nielsen. 2003. Environment classifiers. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages New Orleans Louisisana USA January 15-17 2003 Alex Aiken and Greg Morrisett.(Eds.). ACM 26-37. doi:10.1145\/604131.604134","DOI":"10.1145\/604131.604134"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Fei Wang Daniel Zheng James Decker Xilun Wu Gr\u00e9gory M. Essertel and Tiark Rompf. 2019. Demystifying differentiable programming: shift\/reset the penultimate backpropagator. Proc. ACM Program. Lang. 3 ICFP Article 96 (July 2019) 31 pages. doi:10.1145\/3341700","DOI":"10.1145\/3341700"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Edwin Westbrook Mathias Ricken Jun Inoue Yilong Yao Tamer Abdelatif and Walid Taha. 2010. Mint: Java multi-stage programming using weak separability. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (Toronto Ontario Canada) (PLDI '10). Association for Computing Machinery New York NY USA 400-411. doi:10.1145\/1806596.1806642","DOI":"10.1145\/1806596.1806642"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Ningning Xie Matthew Pickering Andres L\u00f6h Nicolas Wu Jeremy Yallop and Meng Wang. 2022. Staging with class: a specification for typed template Haskell. Proc. ACM Program. Lang. 6 POPL (2022) 1-30. doi:10.1145\/3498723","DOI":"10.1145\/3498723"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","unstructured":"Ningning Xie Leo White Olivier Nicole and Jeremy Yallop. 2023. MacoCaml: Staging Composable and Compilable Macros. Proc. ACM Program. Lang. 7 ICFP Article 209 (Aug. 2023) 45 pages. doi:10.1145\/3607851","DOI":"10.1145\/3607851"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Jeremy Yallop. 2017. Staged generic programming. Proc. ACM Program. Lang. 1 ICFP Article 29 (Aug. 2017) 29 pages. doi:10.1145\/3110273","DOI":"10.1145\/3110273"},{"key":"e_1_3_2_46_1","unstructured":"Jeremy Yallop and community contributors. 2025. effects-bibliography: A collaborative bibliography of work related to the theory and practice of computational effects. GitHub repository. https:\/\/github.com\/yallop\/effects-bibliography"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","unstructured":"Jeremy Yallop and Oleg Kiselyov. 2019. Generating mutually recursive definitions. In Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation.(Cascais Portugal) (PEPM 2019). Association for Computing Machinery New York NY USA 75-81. doi:10.1145\/3294032.3294078","DOI":"10.1145\/3294032.3294078"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","unstructured":"Jeremy Yallop Ningning Xie and Neel Krishnaswami. 2023. flap: A Deterministic Parser with Fused Lexing. Proc. ACM Program. Lang. 7 PLDI Article 155 (June 2023) 24 pages. doi:10.1145\/3591269","DOI":"10.1145\/3591269"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776681","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:40:41Z","timestamp":1784209241000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776681"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776681"],"URL":"https:\/\/doi.org\/10.1145\/3776681","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"}}]}}