SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 15:30 - 16:00 at Lecture Theatre 2 - Effects Chair(s): Peter Thiemann

Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present System C, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate System C in an implementation and prove its soundness.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
EffectsOOPSLA at Lecture Theatre 2
Chair(s): Peter Thiemann University of Freiburg, Germany
15:30
30m
Research paper
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
OOPSLA
Jonathan Immanuel Brachthäuser University of Tübingen, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL
DOI
16:00
30m
Talk
First-class Names for Effect Handlers
OOPSLA
Ningning Xie University of Toronto, Youyou Cong Tokyo Institute of Technology, Kazuki Ikemori Tokyo Institute of Technology, Daan Leijen Microsoft Research
DOI
16:30
30m
Talk
High-Level Effect Handlers in C++
OOPSLA
Dan Ghica Huawei, Sam Lindley University of Edinburgh, Marcos Maronas Bravo Huawei, Maciej Piróg Huawei
DOI