When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion (Extended Version)
Jun Tan, Guannan Wei
cs.PL
Jun 29, 2026 · v2
TL;DR
Mechanizes two typed two-stage calculi and their semantics-preservation metatheory, including binary logical relations, in Lean 4 (about 22k lines).
Abstract
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 $λ^{ref}_{|2|}$, the latter supporting mutable references in the second stage. Their dynamic semantics models 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 $t_1$ evaluates to a value $\mathsf{code} t_2$, then $t_2$ is contextually equivalent to the stage-erasure of $t_1$. 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.
Problem
Staging annotations in typed multi-stage languages can change evaluation order. A staged program may then behave differently from its unstaged counterpart when effects such as divergence or mutable state are present. The open question, posed by Inoue and Taha, is when staging annotations preserve semantics.
Approach
The authors design two statically typed two-stage calculi, λ|2| and λref|2|; the second allows mutable references in the second stage only. Both use automatic let-insertion, tracked as a control effect in a lightweight type-and-effect system. Step-indexed binary logical relations are used to prove that generated code is contextually equivalent to the stage-erasure of the source program. The calculi and metatheory are mechanized in Lean 4 using a locally nameless representation with de Bruijn levels.
Results
For well-typed programs, the authors prove type soundness and strong semantics preservation: generated code is contextually equivalent to the erased program. All results are machine-checked in Lean, at about 10k lines for λ|2| and 11.8k lines for λref|2|.
| Component | λ\ | 2\ | | λref\ | 2\ | |
|---|
| Syntax | 2k | 2.5k |
| LogicalEquiv | 1.9k | 2k |
| SemanticsPreservation | 1.4k | 1.7k |
| Total | 10k | 11.8k |
Summary of the mechanization in Lean (LoC)