Reference. S4 modal sequent calculus as intermediate logic and intermediate language
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.
Cite
Cites 24 works (3 here)
With notes (3)
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Focalisation and Classical Realisability munchmaccagnoni-2009-focalisation
A mixed linear and non-linear logic: Proofs, terms and models: Extended abstract bentonMixedLinearNonlinear1995
Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (‘of course’) modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model.
External (21)
- Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation (2025)
- Mixing classical and intuitionistic constructiveness: a formulae-as-types interpretation for classical S4 modal logic and second-class continuations (Master's thesis) (2025)
- Compiling with continuations, or without? whatever (2019)
- Compiling without continuations (2017)
- Note on Curry's style for Linear Call-by-Push-Value (2017)
- Dual-context calculi for modal logic (2017)
- Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect (2016)
- Sequent calculus as a compiler intermediate language (2016)
- Syntax and Models of a non-Associative Composition of Programs and Proofs (2013)
- Contextual modal type theory (2008)
- A Modal Foundation for Secure Information Flow (2004)
- Etude de la polarisation en logique (PhD thesis) (2002)
- An interpretation of the intuitionistic propositional calculus (1933f) (2001)
- A modal analysis of staged computation (2001)
- Constructive Classical Logic as CPS-Calculus (2000)
- A new deconstructive logic: linear logic (1997)
- On the Unity of Logic (1993)
- A new constructive logic: classic logic (1991)
- A formulae-as-type notion of control (1989)
- RABBIT: A Compiler for SCHEME (Master's thesis) (1978)
- Some theorems about the sentential calculi of Lewis and Heyting (1948)