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.

翻译：在这篇短文中，我们主张基于延续的中介语言对应于中介逻辑的观点。中介语言的目标是作为编译器中间表示的基础，使其能够表示用于优化和编译的富有表达力的程序变换，同时保持使程序能够被高效编译的基本特性，例如延续的“可堆叠性”。中介逻辑是在可证性意义上介于直觉主义逻辑与经典逻辑之间的逻辑系统。基于CPS的中介语言中使用的第二类延续对应于一种经典模态逻辑S4，并附加了蕴含只能返回模态类型的限制。这确实对应于一种中介逻辑，依据的是哥德尔-麦金西-塔斯基定理，该定理指出S4模态片段具有直觉主义特性。我们为S4引入了一种三类别极化序列演算，并配合一个将堆与栈分离的操作机器模型。借助该模型，我们研究了S4模态片段的可堆叠性性质。