Under the Curry--Howard isomorphism, the syntactic structure of programs can be modeled using birelational Kripke structures equipped with intuitionistic and modal relations. Intuitionistic relations capture scoping through persistence, reflecting the availability of resources from outer scopes, while modal relations model resource isolation introduced for various purposes. Traditional modal languages, however, describe only modal transitions and thus provide limited support for expressing fine-grained control over resource availability. Motivated by this limitation, we introduce \emph{Bounded Modal Logic (\textbf{BML})}, an experimental extension of constructive modal logic whose language explicitly accounts for both intuitionistic and modal transitions. We present a natural-deduction proof system and a Kripke semantics for \textbf{BML}, together with a Curry--Howard interpretation via a corresponding typed lambda-calculus. We establish metatheoretic properties of the calculus, showing that \textbf{BML} forms a well-disciplined logical system. This provides theoretical support for our proposed perspective on fine-grained resource control in programming languages.

翻译：在Curry-Howard同构下，程序的语法结构可以通过配备直觉关系和模态关系的双关系Kripke结构进行建模。直觉关系通过持续性捕捉作用域，反映外部作用域中资源的可用性；而模态关系则为各种目的引入的资源隔离建立模型。然而，传统模态语言仅描述模态转换，因此在表达对资源可用性的细粒度控制方面支持有限。受此局限性的启发，我们提出《有界模态逻辑（BML）》——一种构造性模态逻辑的实验性扩展，其语言明确同时处理直觉转换和模态转换。我们为BML提出自然演绎证明系统和Kripke语义学，并通过相应的类型化lambda演算给出Curry-Howard解释。我们建立了该演算的元理论性质，证明BML构成一个良好规约的逻辑系统。这为我们提出的编程语言细粒度资源控制视角提供了理论支撑。