  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.
