一句话：首次形式化研究动态作用域外泄检查，提出并验证 Cause-for-Concern 检查，并与静态环境分类器比较表达力。
元编程与 effect handler 的交互可能导致作用域外泄，即生成作用域非法的代码。静态类型系统可提前阻止外泄，但在实际实现与可用性上存在困难；动态检查已在 MetaOCaml 等系统中使用，却缺乏理论研究，语言设计者难以获得设计指导。本文首次对动态作用域外泄检查进行形式化研究，提出演算 λ⟨⟨op⟩⟩ 以描述和评估不同检查。作者还提出新的动态检查“Cause-for-Concern”，证明其正确性，给出不依赖实现的刻画，并论证其综合既有动态检查的优点。最后，论文用精化环境分类器扩展该框架，静态地防止作用域外泄，并比较其与动态检查的表达力。
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 ( λ ⟨ ⟨ o p ⟩ ⟩ ) 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LeeXKY26,
title = {Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks},
author = {Michael Lee and Ningning Xie and Oleg Kiselyov and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776681}
}