S4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
summary
Claims that second-class continuations correspond to a restricted S4 modal fragment where implications may only return modal types, and that this fragment sits strictly between intuitionistic and classical logic via the Gödel–McKinsey–Tarski embedding. Introduces a three-kinded polarized sequent calculus and a machine semantics that separates a heap vs stack, allocates modal (first-class) values on the heap and continuations on the stack, proves a stackability property and shows translations that factorize CPS and sequent-core style IRs.
AI-written summary · about
chapters (8)
- 0:00S4 modal sequent calculus intro
- 1:17Continuations in compilation
- 3:49Sequent calculus IRs
- 5:14Polarized sequent calculus
- 7:23Stack semantics
- 9:30Intermediate logic
- 10:54Future work: dual modalities
- 11:36Q&A
related talks
12mA Unified View of Modalities in Type Systems
30mContinuations and Coexponentials
13mCompiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
15mCompiling with Continuations, Correctly
19mCombining Dependency, Grades, and Adjoint Logic
18mA modal deconstruction of Löb induction
26mTemporal refinements for Call-By-Push-Value with fixpoint
15mStable Relations and Abstract Interpretation of Higher-Order Programs