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 SepDisplayed time zone: Belfast change
15:30 - 16:30
|Programming a Web Server with Algebraic Effects
Daan Leijen Microsoft Research
|Logical Relations for Algebraic Effects