Andrej Bauer ; Matija Pretnar - An Effect System for Algebraic Effects and Handlers

lmcs:1153 - Logical Methods in Computer Science, December 10, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:9)2014
An Effect System for Algebraic Effects and Handlers

Authors: Andrej Bauer ; Matija Pretnar ORCID-iD

    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.


    Volume: Volume 10, Issue 4
    Published on: December 10, 2014
    Accepted on: June 25, 2015
    Submitted on: February 18, 2014
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1145/3009837.3009897
    Source : ScholeXplorer IsReferencedBy HANDLE 20.500.11820/bd2598b0-20ce-4272-821f-985974bdd4f6
    • 10.1145/3009837.3009897
    • 10.1145/3009837.3009897
    • 10.1145/3009837.3009897
    • 20.500.11820/bd2598b0-20ce-4272-821f-985974bdd4f6
    Do be do be do
    Lindley, Sam ; McBride, Conor ; McLaughlin, Craig ;

    23 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 1418 times.
    This article's PDF has been downloaded 531 times.