Paper accepted for publication at OOPSLA 2023

Our paper “Continuation-Passing to Direct Style: Typed and Tight” (Marius Müller, Philipp Schuster
Researcher
Philipp Schuster
, Jonathan Brachthäuser
Head of the SE research group
Jonathan 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

Back to Direct Style: Typed and Tight

by Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann

In Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2023.

Learn More