This program is tentative and subject to change.

Fri 25 Oct 2024 17:00 - 17:20 at Pasadena - Effects

Lexically scoping effect handlers is a language-design idea that equips algebraic effects with a modular semantics: it enables local-reasoning principles without giving up on the control-flow expressiveness that makes effect handlers powerful. However, we observe that existing implementations risk incurring costs akin to the run-time search for dynamically scoped handlers. This paper presents a compilation strategy for lexical effect handlers, adhering to the lexical scoping principle and targeting a language with low-level control over stack layout. Key aspects of this approach are formalized and proven correct. We embody the ideas in a language called Lexa: the Lexa compiler translates high-level effect handling to low-level stack switching. We evaluate the Lexa compiler on a set of benchmarks; the results suggest that it generates efficient code, reducing running-time complexity from quadratic to linear in some cases.

This program is tentative and subject to change.

Fri 25 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
16:00
20m
Talk
Effect handlers for C via coroutines
OOPSLA 2024
Mario Alvarez-Picallo Huawei Research Centre, Teodoro Freund Huawei Research Centre, Dan Ghica Huawei, Sam Lindley University of Edinburgh
16:20
20m
Talk
Effects and Coeffects in Call-By-Push-Value
OOPSLA 2024
Cassia Torczon University of Pennsylvania, Emmanuel Suarez Acevedo Cornell University, Shubh Agrawal University of Michigan, Joey Velez-Ginorio , Stephanie Weirich University of Pennsylvania
16:40
20m
Talk
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
OOPSLA 2024
Taro Sekiyama National Institute of Informatics; SOKENDAI, Hiroshi Unno Tohoku University
17:00
20m
Talk
Lexical Effect Handlers, Directly
OOPSLA 2024
Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Edward Lee University of Waterloo, Yizhou Zhang University of Waterloo
17:20
20m
Talk
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
OOPSLA 2024
Noam Zilberstein Cornell University, Angelina Saliling Cornell University, Alexandra Silva Cornell University