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

Displayed time zone: Belfast change

15:30 - 16:30
EffectsHOPE at L3
Programming a Web Server with Algebraic Effects
Daan Leijen Microsoft Research
Logical Relations for Algebraic Effects
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk , Filip Sieczkowski University of Wrocław