文章基本信息

标题：A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers
本地全文：下载
作者：Dariusz Biernacki ; Lenglet, Sergueï ; Piotr Polesiuk 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：7:1-7:22
DOI：10.4230/LIPIcs.FSCD.2020.7
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：algebraic effect; handler; behavioral equivalence; bisimilarity