SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal

This program is tentative and subject to change.

Fri 27 Oct 2023 14:00 - 14:15 at Room II - compilation and optimization 1

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.

This program is tentative and subject to change.

Fri 27 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
compilation and optimization 1OOPSLA at Room II
14:00
15m
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:15
15m
Talk
Rapid: Region-based Pointer Disambiguation
OOPSLA
Khushboo Chitre IIIT Delhi, Piyus Kedia IIIT Delhi, Rahul Purandare University of Nebraska-Lincoln
14:30
15m
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
Pre-print
14:45
15m
Talk
Formally Verifying Optimizations with Block Simulations
OOPSLA
Leo Gourdin Université Grenoble-Alpes, Benjamin Bonneau ENS PSL, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Alexandre Bérard Université Grenoble-Alpes
DOI Pre-print
15:00
15m
Talk
Hardware-Aware Static Optimization of Hyperdimensional Computations
OOPSLA
Pu (Luke) Yi Stanford University, Sara Achour MIT