Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: Maciej Piróg: Handle with care: relational interpretation of algebraic effects and handlers

LFCS seminar: Maciej Piróg: Handle with care: relational interpretation of algebraic effects and handlers

— filed under: ,

What
  • LFCS Seminar
  • Upcoming events
When Dec 08, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal
iCal

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. 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. This is joint work with Dariusz Biernacki, Piotr Polesiuk, and Filip Sieczkowski.

Document Actions