2026/02/10 by Yuito Murase, Akinori Maniwa
Computer Science · #cs.LO
It is widely known that proof systems for modal logic can be interpreted as type systems for multi-stage programming (MSP). However, existing modal-logical foundations for MSP do not fully account for staged programs with complex scoping structures. For example, a modal account of cross-stage persistence, in which free variables in generated code may refer to run-time bindings, has not yet been fully established. This paper presents *Bounded Modal Logic* (BML), a constructive modal logic with modalities bounded by names for scopes and first-order-style quantification over those names. This makes scope dependencies of code fragments explicit, thereby enabling reasoning about staged programs with nontrivial scoping behavior, including cross-stage persistence. We present a natural deduction system and a Kripke semantics for BML, and prove their soundness and completeness. We also provide a computational counterpart of BML as a typed lambda calculus for MSP. In addition to standard metatheoretic properties such as confluence and strong normalization, we develop a staged semantics for the calculus, showing that the type system supports the stage-by-stage execution model required for multi-stage programming.