文章基本信息

标题：An Effect System for Algebraic Effects and Handlers
本地全文：下载
作者：Andrej Bauer ; Matija Pretnar
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2014
卷号：10
期号：4
页码：1
DOI：10.2168/LMCS-10(4:9)2014
出版社：Technical University of Braunschweig
摘要：We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.
其他关键词：algebraic effects, effect handlers, effect system.