Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 09:00 - 09:22 at Sala I - Type Abstraction and Effects Chair(s): Benjamin Delaware

Algebraic effect handlers offer a unified approach to expressing control-flow transfer idioms such as exceptions, iteration, and async/await. Unfortunately, previous attempts to make these handlers type-safe have failed to support the fundamental principle of modular reasoning for higher-order abstractions. We demonstrate that abstraction-safe algebraic effect handlers are possible by giving them a new semantics. The key insight is that code should only handle effects it is aware of. In our approach, the type system guarantees all effects are handled, but it is impossible for higher-order, effect-polymorphic code to accidentally handle effects raised by functions passed in; such effects tunnel through the higher-order, calling procedures polymorphic to them. By contrast, the possibility of accidental handling threatens previous designs for algebraic effect handlers. We prove that our design is not only type-safe, but also abstraction-safe. Using a logical-relations model that we prove sound with respect to contextual equivalence, we derive previously unattainable program equivalence results. Our mechanism offers a viable approach for future language designs aiming for effect handlers with strong abstraction guarantees.

Thu 17 Jan

Displayed time zone: Belfast change

09:00 - 10:06
Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin Delaware Purdue University
09:00
22m
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou Zhang Cornell University, Andrew Myers Cornell University
Link to publication DOI Media Attached
09:22
22m
Talk
Abstracting Algebraic Effects
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication DOI Media Attached
09:44
22m
Talk
Fully Abstract Module Compilation
Research Papers
Karl Crary Carnegie Mellon University
Link to publication DOI Media Attached File Attached