{"ID":5439491,"CreatedAt":"2026-07-01T01:17:58.482524686Z","UpdatedAt":"2026-07-02T19:06:01.127452785Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2606.30854","arxiv_id":"2606.30854","title":"When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-Stage Programming with Let-Insertion (Extended Version)","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.","short_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, Meta...","url_abs":"https://arxiv.org/abs/2606.30854","url_pdf":"https://arxiv.org/pdf/2606.30854v1","authors":"[\"Jun Tan\",\"Guannan Wei\"]","published":"2026-06-29T19:34:31Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[]","has_code":false}