一句话：提出两种带效应追踪的两阶段演算，以自动 let 插入保持语义，并机械化证明分阶段程序与其去阶段化版本上下文等价。
多阶段编程允许程序员将代码当作数据，在生成期对代码片段做语法操作，但这种操作会微妙地改变求值顺序，使分阶段程序与常作为参考实现的去阶段化程序语义不一致，既妨碍正确性推理，也使其无法直接替换去阶段化版本。本文研究带语义保持保证的多阶段语言设计，提出两个静态类型的两阶段演算 λ|2| 与 λ|2|^ref，后者在第二阶段支持可变引用。其动态语义对自动 let 插入建模，并通过轻量级类型-效应系统把插入追踪为控制效应，从而对带效应的代码片段进行类型安全且保持语义的操作。作者用二元逻辑关系证明强语义保持定理：若良类型的两阶段程序 t1 求值为代码值 t2，则 t2 与 t1 的去阶段化结果上下文等价。该工作机械化验证了演算的元理论，回答了 Inoue 与 Taha 关于分阶段注解何时保持语义的问题，并为语义保持的多阶段编程奠定基础。
Multi-stage programming with quotations has long provided a powerful way to generate and manipulate code. By treating code as data, programmers can write multi-stage programs in which earlier stages produce specialized code from inputs available at generation time. Modern typed multi-stage languages (e.g., MetaML, MetaOCaml, Template Haskell, and Scala 3) adopt quotation/splicing constructs while enforcing the well-typedness of generated code. However, manipulating code fragments syntactically can subtly change evaluation order, leading to semantic discrepancies between a staged program and its unstaged counterpart, which is intended to serve as a reference implementation in many cases. The inconsistency complicates reasoning about correctness, and prevents staged code from being a drop-in replacement for its unstaged counterpart. In this paper, we study the design of multi-stage languages with semantics preservation guarantees. We develop two statically typed two-stage calculi, 𝜆|2| and 𝜆|2|^ref, the latter supporting mutable references in the second stage. Their dynamic semantics model automatic let-insertion, tracked as a control effect in a lightweight type-and-effect system, enabling type-safe and semantics-preserving manipulation of effectful code fragments. We develop binary logical relations to prove strong semantics-preservation theorems: if a well-typed two-stage program t1 evaluates to a value code t2, then t2 is contextually equivalent to the stage-erasure of t1. Our calculi and their mechanized metatheory provide a simple and definitive answer to the question posed by Inoue and Taha of when staging annotations preserve semantics, and lay a foundation for future work on semantics-preserving multi-stage programming.
@article{paperbot12108,
title = {When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion},
author = {Jun Tan and Guannan Wei},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839477}
}