Semantics Club 26 01 2001

Adequacy for Algebraic Effects

John Power

(joint work with Gordon Plotkin)


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.