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.
Fri 27 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|Formally Verifying Optimizations with Block Simulations
Léo Gourdin Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Benjamin Bonneau Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Sylvain Boulmé Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag, Alexandre Bérard Université Grenoble Alpes - CNRS - Grenoble INP - VerimagDOI Pre-print
|Back to Direct Style: Typed and Tight
Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of TübingenDOI Pre-print
|Hardware-Aware Static Optimization of Hyperdimensional Computations
|Rapid: Region-Based Pointer Disambiguation
|Automated Ambiguity Detection in Layout-Sensitive Grammars
Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA - Helmholtz Center for Information Security, Fei He Tsinghua UniversityDOI Pre-print