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 (GMT+01:00) Greenwich Mean Time : Belfast change
|15:30 - 16:00|
Daan LeijenMicrosoft Research
|16:00 - 16:30|