*Semantics Club 26 01 2001*

# Adequacy for Algebraic Effects

## John Power

(joint work with Gordon Plotkin)### Abstract

Moggi proposed a unified category-theoretic account of computational effects
based upon a category with finite products together with a strong monad
on it for which Kleisli exponentials exist. He introduced the computational
lambda-calculus, a core call-by-value functional
programming language for effects, for which the Kleisli
categories as above form a sound and complete class of models. But the
computational lambda calculus contains neither operations nor operational
semantics. So we introduce them for algebraic effects, where the operations
are
given by an algebraic signature, and their semantics is supported by the monad,
in a certain sense. We prove general adequacy theorems and representation
theorems, and we
illustrate with two examples: nondeterminism and probabilistic
nondeterminism.