SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 16:18 - 16:36 at Room I - effect systems Chair(s): Sebastian Erdweg

Effect handlers are a high-level abstraction that enables programmers to use effects in a structured
way. They have gained a lot of popularity within academia and subsequently also in industry. However,
the abstraction often comes with a significant runtime cost and there has been intensive research
recently on how to reduce this price.

A promising approach in this regard is to implement effect handlers using a CPS translation and
to provide sufficient information about the nesting of handlers. With this information the
CPS translation can decide how effects have to be lifted through handlers, i.e., which handlers
need to be skipped, in order to handle the effect at the correct place. A structured way to make
this information available is to use a calculus with a region system and explicit subregion
evidence. Such calculi, however, are quite verbose, which makes them impractical to use as a
source-level language.

We present a method to infer the lifting information for a calculus underlying a source-level language.
This calculus uses second-class capabilities for the safe use of effects. To do so, we define a typed translation
to a calculus with regions and evidence and we show that this lift-inference translation is typability-
and semantics-preserving. On the one hand, this exposes the precise relation between the second-class
property and the structure given by regions. On the other hand, it closes a gap in a compiler pipeline
enabling efficient compilation of the source-level language. We have implemented lift inference in this
compiler pipeline and conducted benchmarks which indicate that the approach is indeed working.

Thu 26 Oct

Displayed time zone: Lisbon change

16:00 - 17:30
effect systemsOOPSLA at Room I
Chair(s): Sebastian Erdweg JGU Mainz
16:00
18m
Talk
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems
OOPSLA
Magnus Madsen Aarhus University, Jaco van de Pol Aarhus University, Troels Henriksen University of Copenhagen
DOI
16:18
18m
Talk
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
OOPSLA
Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Lindegaard Starup Aarhus University, Klaus Ostermann University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
Link to publication DOI Pre-print
16:36
18m
Talk
Gradual Typing for Effect Handlers
OOPSLA
Max S. New University of Michigan, Eric Giovannini University of Michigan, Daniel R. Licata Wesleyan University
DOI
16:54
18m
Talk
When Concurrency Matters: Behaviour-Oriented Concurrency
OOPSLA
Luke Cheeseman Imperial College London, Matthew J. Parkinson Microsoft Azure Research, Sylvan Clebsch Microsoft Azure Research, Marios Kogias Imperial College London; Microsoft Research, Sophia Drossopoulou Imperial College London, David Chisnall Microsoft, Tobias Wrigstad Uppsala University, Paul Liétar Imperial College London
DOI
17:12
18m
Talk
Continuing WebAssembly with Effect Handlers
OOPSLA
Luna Phipps-Costin Northeastern University, Andreas Rossberg Independent, Arjun Guha Northeastern University; Roblox, Daan Leijen Microsoft Research, Daniel Hillerström Huawei Zurich Research Center, KC Sivaramakrishnan Tarides; IIT Madras, Matija Pretnar University of Ljubljana, Sam Lindley University of Edinburgh
DOI Pre-print