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.