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 $λ○▷$, an extension of
$λ○▷pat$ 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.