一句话：提出带 let-splice 绑定的多阶段演算 λ○▷，用上下文模态类型系统支持 splice 变量，并扩展到代码模式匹配。
多阶段编程通过 quote-and-splice 支持类型化元编程，但传统语法难以管理表达式求值，并给代码模式匹配等高级特性带来复杂机制。本文提出多阶段演算 λ○▷，引入 let-splice 绑定，将 splice 表达式显式绑定到 splice 变量，从而灵活地管理、共享和复用 splice 计算。受上下文模态类型论启发，类型系统为类型关联类型上下文，以刻画 splice 变量的变量依赖。该机制可扩展到代码模式匹配与重写，形成 λ○▷pat。作者证明两个演算的语法类型可靠性，并用 Kripke 风格模型给出指称语义与 adequacy 结果；所有证明均在 Agda 中机器化。
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.