S4 modal sequent calculus as intermediate logic and intermediate language

TL;DR

This paper explores the connection between continuation-based intermediate languages and intermediate logics, specifically using S4 modal logic to model program transformations and compiler optimizations.

Contribution

It introduces a three-kinded polarized sequent calculus for S4 and an operational machine model that separates heap and stack, linking logic and compiler design.

Findings

S4 modal logic models continuation-based intermediate languages.

A sequent calculus for S4 with polarisation is developed.

Stackability properties are studied within the modal logic framework.

Abstract

In this short paper, we advocate for the idea that continuation-based intermediate languages correspond to intermediate logics. The goal of intermediate languages is to serve as a basis for compiler intermediate representations, allowing to represent expressive program transformations for optimisation and compilation, while preserving the properties that make programs compilable efficiently in the first place, such as the "stackability" of continuations. Intermediate logics are logics between intuitionistic and classical logic in terms of provability. Second-class continuations used in CPS-based intermediate languages correspond to a classical modal logic S4 with the added restriction that implications may only return modal types. This indeed corresponds to an intermediate logic, owing to the G\"odel-McKinsey-Tarski theorem which states the intuitionistic nature of the modal fragment of S4. We introduce a three-kinded polarised sequent calculus for S4, together with an operational machine model that separates a heap from a stack. With this model we study a stackability property for the modal fragment of S4.