Bounded Modal Logic

TL;DR

This paper introduces Bounded Modal Logic (BML), an extension of constructive modal logic that explicitly models resource scoping and isolation, supported by a proof system, semantics, and Curry--Howard interpretation.

Contribution

We develop BML, a new logic that explicitly captures both intuitionistic and modal resource transitions, with a proof system, semantics, and typed lambda-calculus.

Findings

BML provides a well-structured logical framework.

The proof system and semantics are sound and complete.

BML supports fine-grained resource control in programming languages.

Abstract

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.