Skip to Main content Skip to Navigation
Conference papers

A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers

Abstract : We present a complete coinductive syntactic theory for an untyped calculus of algebraic operations and handlers, a relatively recent concept that augments a programming language with unprecedented flexibility to define, combine and interpret computational effects. Our theory takes the form of a normal-form bisimilarity and its soundness w.r.t. contextual equivalence hinges on using so-called context variables to test evaluation contexts comprising normal forms other than values. The theory is formulated in purely syntactic elementary terms and its completeness demonstrates the discriminating power of handlers. It crucially takes advantage of the clean separation of effect handling code from effect raising construct, a distinctive feature of algebraic effects, not present in other closely related control structures such as delimited-control operators.
Document type :
Conference papers
Complete list of metadata
Contributor : Sergueï Lenglet <>
Submitted on : Thursday, April 30, 2020 - 11:49:01 AM
Last modification on : Saturday, November 21, 2020 - 9:54:03 AM


Files produced by the author(s)




Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk. A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.7⟩. ⟨hal-02559253⟩



Record views


Files downloads