SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 14:18 - 14:36 at Room II - compilation and optimization 1 Chair(s): Will Crichton

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 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
compilation and optimization 1OOPSLA at Room II
Chair(s): Will Crichton Brown University
14:00
18m
Talk
Formally Verifying Optimizations with Block Simulations
OOPSLA
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 - Verimag
DOI Pre-print
14:18
18m
Talk
Back to Direct Style: Typed and Tight
OOPSLA
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übingen
DOI Pre-print
14:36
18m
Talk
Hardware-Aware Static Optimization of Hyperdimensional Computations
OOPSLA
Pu (Luke) Yi Stanford University, Sara Achour Stanford University
DOI
14:54
18m
Talk
Rapid: Region-Based Pointer Disambiguation
OOPSLA
Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln
DOI
15:12
18m
Talk
Automated Ambiguity Detection in Layout-Sensitive Grammars
OOPSLA
Jiangyi Liu Tsinghua University, Fengmin Zhu CISPA - Helmholtz Center for Information Security, Fei He Tsinghua University
DOI Pre-print