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.

This publication is related to the Compiling with Continuations research project.

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.

Talk

Video recording of the talk available on YouTube.

News

Three Papers at OOPSLA 2023

Together with our collaborators the SE group presents three different papers at this year’s International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023).

Read more ...

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).

Read more ...