有界模态逻辑
Bounded Modal Logic: Explicit Scope Dependencies in Multi-Stage Programming
AI总结：
有界模态逻辑通过结合直觉和模态转换，提供细粒度资源控制的理论支持。
摘要：
在 Curry-Howard 同构性下，程序的语法结构可以使用配备直觉和模态关系的双关系 Kripke 结构来建模。直觉关系通过持久性捕捉作用域，反映从外层作用域中资源的可用性，而模态关系则建模为各种目的引入的资源隔离。然而，传统的模态语言只能描述模态转换，因此在表达对资源可用性的细粒度控制方面支持有限。受此限制的启发，我们引入了有界模态逻辑（BML），这是一种构造性模态逻辑的实验性扩展，其语言明确考虑了直觉和模态转换。我们为 BML 提供了自然演绎证明系统和 Kripke 语义，以及通过相应的类型 lambda 计算机进行的 Curry-Howard 解释。我们建立了该算法的元理论性质，证明 BML 形成一个良好的逻辑系统。这为我们在编程语言中提出的细粒度资源控制观点提供了理论支持。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
