Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bounded Modal Logic

Yuito Murase, Akinori Maniwa

TL;DR

The paper tackles fine-grained resource control in programming languages by extending constructive modal logic with a birelational Kripke semantics and a bounded modality, yielding Bound Modal Logic ($BML$). It provides a formal $-structure$ as semantic grounding, a natural-deduction system, a Kripke semantics, and a Curry–Howard interpretation via a modal lambda-calculus, with metatheoretic results establishing soundness and completeness. $BML$ is shown to generalize $CS4$ both semantically and proof-theoretically and supports polymorphic classifier quantification, enabling reasoning over code fragments with arbitrary scopes. Together, these results offer a theoretical foundation for fine-grained resource control in MSP and other resource-sensitive programming contexts, connecting logic with practical programming semantics.

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.

Bounded Modal Logic

TL;DR

The paper tackles fine-grained resource control in programming languages by extending constructive modal logic with a birelational Kripke semantics and a bounded modality, yielding Bound Modal Logic (). It provides a formal as semantic grounding, a natural-deduction system, a Kripke semantics, and a Curry–Howard interpretation via a modal lambda-calculus, with metatheoretic results establishing soundness and completeness. is shown to generalize both semantically and proof-theoretically and supports polymorphic classifier quantification, enabling reasoning over code fragments with arbitrary scopes. Together, these results offer a theoretical foundation for fine-grained resource control in MSP and other resource-sensitive programming contexts, connecting logic with practical programming semantics.

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.
Paper Structure (2 sections, 3 equations, 5 figures)

This paper contains 2 sections, 3 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Syntactic Structure of Modal Lambda-Terms

Figures (5)

  • Figure 1: Kripke structure of lambda-terms. Here, and represent intuitionistic and modal relations, respectively.
  • Figure 2: Tautologies in . $\mathord{\boldsymbol{!} }$ represents global scope, and $\mathbf{FC} ( \mathit{A} )$ is a set of classifiers occurs freely in $\mathit{A}$.
  • Figure 3: Hyp
  • Figure 4: $\Box$-I
  • Figure 5: $\Box$-E

Theorems & Definitions (1)

  • Definition 3: -Structure