Multi-stage programming is a popular approach to typed meta-programming, reducing abstraction overhead and producing performant programs. However, the traditional quote-and-splice staging syntax, as introduced by Rowan Davies in 1996, can introduce complexities in managing expression evaluation, and also often necessitates sophisticated mechanisms for advanced features such as code pattern matching. This paper introduces λ ○▷ , a novel staging calculus featuring let-splice bindings, a construct that explicitly binds splice expressions to splice variables, providing flexibility in managing, sharing, and reusing splice computations. Inspired by contextual modal type theory, our type system associates types with a typing context to capture variables dependencies of splice variables. We demonstrate that this mechanism seamlessly scales to features like code pattern matching, by formalizing λ ○▷ pat , an extension of λ ○▷ with code pattern matching and rewriting. We establish the syntactic type soundness of both calculi. Furthermore, we define a denotational semantics using a Kripke-style model, and prove adequacy results. All proofs have been fully mechanized using the Agda proof assistant.

@article{paperbot3051,
  title = {Multi-stage Programming with Splice Variables},
  author = {Tsung-Ju Chiang and Ningning Xie},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {ICFP},
  year = {2025},
  doi = {10.1145/3747518}
}