Wed 10 Jan 2018 11:45 - 12:10 at Watercourt - Types and Effects Chair(s): Neel Krishnaswami

Algebraic effects and handlers have received a lot of attention recently, both from the theoretical point of view and in practical language design. This stems from the fact that algebraic effects give the programmer unprecedented freedom to define, combine, and interpret computational effects. This plenty-of-rope, however, demands not only a deep understanding of the underlying semantics, but also access to practical means of reasoning about effectful code, including correctness and program equivalence. In this paper we tackle this problem by constructing a step-indexed relational interpretation of a call-by-value calculus with algebraic effect handlers and row-based polymorphic type-and-effect system. Our calculus, while striving for simplicity, enjoys desirable theoretical properties, and is close to the cores of programming languages with algebraic effects used in the wild, while the logical relation we build for it can be used to reason about non-trivial properties, such as contextual equivalence and contextual approximation of programs. Our development has been fully formalised in the Coq proof assistant.

Wed 10 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

10:30 - 12:10: Research Papers - Types and Effects at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
POPL-2018-papers10:30 - 10:55
Jean-Philippe BernardyUniversity of Gothenburg, Mathieu BoespflugTweag I/O, Ryan R. NewtonIndiana University, Simon Peyton JonesMicrosoft Research, Arnaud SpiwackTweag I/O
Pre-print File Attached
POPL-2018-papers10:55 - 11:20
POPL-2018-papers11:20 - 11:45
Danel AhmanInria Paris
POPL-2018-papers11:45 - 12:10
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław