Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 16:00 - 16:30 at L3 - Effects

We present a logical relation for reasoning about contextual equivalence and contextual approximation of programs in a language with algebraic effect handlers and row-based polymorphic type-and-effect system. We start with a state-of-the-art programming language with algebraic effects, Leijen’s Koka, identify the challenging subset of the calculus and use the standard technique of biorthogonality to build a step-indexed relational interpretation that allows us to reason about approximation and equivalence, as well as show soundness of the type system. We are then able to use the relation to show equivalence of various programs (including equivalence of pure and effectful code), as well as some interesting type-directed equivalences.

Sun 3 Sep

15:30 - 16:30: HOPE 2017 - Effects at L3
hope-2017-talks150444540000015:30 - 16:00
Daan LeijenMicrosoft Research
hope-2017-talks150444720000016:00 - 16:30
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr Polesiuk, Filip SieczkowskiUniversity of Wrocław