ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

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 Davies 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 \textit{let-splice bindings}, a construct that explicitly binds splice expressions to \textit{splice variables}, providing flexibility in managing, sharing, and reusing splice computations. Inspired by \textit{contextual modal type theory}, our type system associates types with a typing context to capture \textit{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.