Relational Interpretation of Algebraic Effects and Handlers

Watch a 22-minute conference presentation from POPL 2018 exploring the theoretical foundations and practical implications of algebraic effects and handlers in programming language design. Dive into the research conducted by University of Wrocław scholars who developed a step-indexed relational interpretation of a call-by-value calculus with algebraic effect handlers and row-based polymorphic type-and-effect system. Learn how this theoretical framework enables reasoning about program equivalence and correctness in effectful code, with the entire development formally verified using the Coq proof assistant. Understand the balance between the flexibility offered by algebraic effects and the need for robust reasoning tools when implementing computational effects in modern programming languages.