When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion

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 welltypedness 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 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 welltyped two-stage program 𝑡 1 evaluates to a value code 𝑡 2 , then 𝑡 2 is contextually equivalent to the stage-erasure of 𝑡 1 . Our calculi and their mechanized metatheory provide a simple and definitive answer to the question posed by Inoue and Taha [27,28] of when staging annotations preserve semantics, and lay a foundation for future work on semantics-preserving multi-stage programming.

• Theory of computation → Type theory.