A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers

Dariusz Biernacki (1) , Sergueï Lenglet (2) , Piotr Polesiuk (1)

1 UWr - University of Wrocław [Poland]
2 MOSEL - Proof-oriented development of computer-based systems

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.

Domaines: Théorie et langage formel [cs.FL]

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⟩