Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

S4 modal sequent calculus as intermediate logic and intermediate language

Jean Caspar, Guillaume Munch-Maccagnoni

TL;DR

The paper links CPS-based intermediate languages to intermediate logics, particularly showing that second-class continuations correspond to a modal logic $S4$ with a restriction to modal-returns. It then develops a polarised sequent calculus $\mathbf{L}^{\Box}_{pol}$ for classical $S4$, along with a three-polarity type system and a machine-like semantics that separates a heap for modal values from a stack, enabling stackability analyses. The authors prove correctness properties such as progress, subject reduction, and strong normalization by translating to a known system $\mathrm{LJ}^{\eta}_p$, establishing a principled bridge between CPS translations, modal logic, and compiler intermediates. The approach provides a theoretically grounded framework for preserving stackability and efficient compilation during program transformations in intermediate representations.

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ödel-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.

S4 modal sequent calculus as intermediate logic and intermediate language

TL;DR

The paper links CPS-based intermediate languages to intermediate logics, particularly showing that second-class continuations correspond to a modal logic with a restriction to modal-returns. It then develops a polarised sequent calculus for classical , along with a three-polarity type system and a machine-like semantics that separates a heap for modal values from a stack, enabling stackability analyses. The authors prove correctness properties such as progress, subject reduction, and strong normalization by translating to a known system , establishing a principled bridge between CPS translations, modal logic, and compiler intermediates. The approach provides a theoretically grounded framework for preserving stackability and efficient compilation during program transformations in intermediate representations.

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ödel-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.
Paper Structure (10 sections, 12 theorems, 11 equations, 5 figures)

This paper contains 10 sections, 12 theorems, 11 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Intermediate languages as intermediate logics
  3. A classical S4 sequent calculus as an intermediate representation
  4. A theory of second-class continuations via S4
  5. System L□pol
  6. Brief recapitulation of the polarised L-calculus.
  7. Adding a polarity $\mathord{\square}$.
  8. Typing
  9. Machine-like semantics
  10. Correctness

Key Result

lemma 1

If $V$ is a value and $\Gamma \mathrel{\textnormal{\textbrokenbar}} \Theta \vdash V : A_{\mathord{\square}} ; \Delta$ then $\Gamma_{\mathord{\square}} \mathrel{\textnormal{\textbrokenbar}} \Theta \vdash V : A_{\mathord{\square}} ; \diamond$.

Figures (5)

  • Figure 1: Operational semantics of system $\mathbf{L}^{\mathord{\Box}}_{{\mathrm{pol}}}$
  • Figure 2: Typing rules of the system $\mathbf{L}^{\mathord{\Box}}_{{\mathrm{pol}}}$
  • Figure 3: Evaluation of values and stacks
  • Figure 4: Evaluation of commands
  • Figure 5: Typing of environments

Theorems & Definitions (12)

  • lemma 1: Modal restriction
  • lemma 2: Typed substitution
  • lemma 3: Subject reduction
  • lemma 4: Normalization
  • theorem 1: Evaluation
  • theorem 2: Stackability
  • lemma 5: Progress
  • lemma 6: Subject reduction
  • lemma 7
  • lemma 8
  • ...and 2 more