Post #1556644

The continuations debate in programming languages can be summarised as follows: one camp debates whether we should use CPS or not for compilation. The other camp believes that the recurrence of the concept of continuation in many places in computer science and logic is revealing a fundamental structure of computation; syntax is not arbitrary, good syntactic artifacts let us get a glimpse of and benefit from this structure underneath. In the paper "Compiling with continuations, or without? Whatever", Cong, Osvald, Essertel and Rompf propose to capture the second-class nature of continuations used in compilation in a type-theoretic way. Seemingly advocating for the first camp, it places itself in the second. Seeking to understand their CPS from the point of view of sequent calculus, Jean Caspar and I propose at PEPM 2026 (this morning) an understanding of their calculus from the point of view of polarised classical S4 sequent calculus. Continuations used in compilation are in-between intuitionistic (linearly-used) and classical (unrestricted use). Polarised S4 realises this mixing of classical and intuitionistic logic due to the Gödel-McKinsey-Tarski theorem which states the intuitionistic nature of the modal fragment of S4. "S4 modal sequent calculus as intermediate logic and intermediate language" (with paper available): https://popl26.sigplan.org/details/pepm-2026-papers/6/S4-modal-sequent-calculus-as-intermediate-logic-and-intermediate-language-Short-Pape