# A Linear-logical Reconstruction of Intuitionistic Modal Logic S4

## TL;DR

This paper develops a novel modal linear logic framework to accurately translate intuitionistic modal logic S4 into linear logic, addressing modality interactions and providing semantics via Geometry of Interaction.

## Contribution

It introduces a modal linear logic that extends intuitionistic multiplicative exponential linear logic to incorporate S4 modalities, enabling a sound translation from IS4.

## Key findings

- Established a sound translation from IS4 to modal linear logic.
- Provided a Geometry of Interaction semantics for the modal lambda-calculus.
- Resolved modality interaction issues in linear logic translation.

## Abstract

We propose a "modal linear logic" to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.