An Effect System for Algebraic Effects and Handlers

Andrej Bauer, Matija Pretnar
6/26/2013
cs.PLcs.LO

Official code: matijapretnar/proofs (19 stars, last commit 2020-02-04).

Abstract

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.

View on arXivView PDF

Code Implementations(1)

matijapretnar/proofsOfficial100%

A collection of mechanised proofs

190AMPL, PythonNov 28, 20136 years ago

Similar Papers

What is algebraic about algebraic effects and handlers?

75% match1 repo1.2k2018

Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts

73% match2023

Causal Laws and Multi-Valued Fluents

73% match2023

ETAS: An Effect-Typed Language for Agent Systems

72% match2026

L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents

72% match2026

Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality

72% match2026

Cite this paper

@article{bauer2013effect,
  title  = {An Effect System for Algebraic Effects and Handlers},
  author = {Andrej Bauer and Matija Pretnar},
  year   = {2013},
  eprint = {1306.6316},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1306.6316}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1306.6316.svg)](https://codeofpaper.com/paper/1306.6316)

Discussion