Our paper “Continuation-Passing to Direct Style: Typed and Tight” (Marius Müller, Philipp Schuster
ResearcherPhilipp Schuster, Jonathan Brachthäuser
Head of the SE research groupJonathan Immanuel Brachthäuser, and Klaus Ostermann) has been accepted for publication at the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023).

Abstract

Translating programs into continuation-passing style is a well-studied tool to explicitly deal with the control structure of programs. This is useful, for example, for compilation.

In a typed setting, there also is a logical interpretation of such a translation as an embedding of classical logic into intuitionistic logic. A naturally arising question is whether there is an inverse translation back to direct style. The answer to this question depends on how the continuation-passing translation is defined and on the domain of the inverse translation. In general, translating programs from continuation-passing style back to direct style requires the use of control operators to account for the use of continuations in non-trivial ways.

We present two languages, one in direct style and one in continuation-passing style. Both languages are typed and equipped with an abstract machine semantics. Moreover, both languages allow for non-trivial control flow.

We further present a translation to continuation-passing style and a translation back to direct style. We show that both translations are type-preserving and also preserve semantics in a very precise way giving an operational correspondence between the two languages.

Moreover, we show that the compositions of the translations are well-behaved. In particular, they are syntactic one-sided inverses on the full language and full syntactic inverses when restricted to trivial control flow.

More about this publication

Publications