The $\lambda$-calculus has long been an essential tool for the study of functional programming languages, where it has been used as the theoretical foundation for understanding key concepts such as binding structures, calling conventions, and continuations. But how exactly does one relate a programming language to a calculus? In his seminal work, Plotkin demonstrates an approach to answer that, by showing how the operational semantics of Landin’s ISWIM coincides with a prefix of the standard reduction sequence derived from the $\lambda$-calculus’ equational theory, which in turn is sound with regard to the observational equivalence in the language.

However, there are situations in which the $\lambda$-calculus, in its usual formulation, is not a perfect match. As an example: for efficient execution, source code is often translated by compilers into some intermediate representation (IR) language, where continuations are more prominent. For functional languages, a common approach is to apply a continuation-passing style (CPS) translation, which gives rise to a class of IRs in which no function application is allowed to return. Unfortunately, Plotkin himself showed that the $\lambda$-calculus is not complete for CPS terms.

We argue that, just as the study of programming languages benefits from a strong theoretical foundation, so would the study of IRs. In the present work, we describe ongoing research on the formalization of Thielecke’s CPS-calculus, which we take as their representative. We equip it with an equational theory based on compiler optimizations, and study its metatheory by borrowing from the literature on both $\lambda$-calculus and $\pi$-calculus. The new reduction relation enjoys a theory of residuals, is confluent, and may be factorized in order to justify its relationship to an actual compiler IR. We hope that these results will, for example, aid in proving optimizations sound.

Finally, we show that the CPS-calculus is strongly normalizing in a simply-typed setting, allowing it to double as a logic system where the primitive is not implication, but rather negation. Its similarity to the negative subset of Laurent’s polarized linear logic allows us to make a case for a Curry-Howard correspondence for IRs, and opens up a new path for safe compilation of programs written in dependently-typed programming languages.