##
**Gordon Plotkin's Invited Lecture**

### Adequacy for Algebraic Effects

###
Gordon Plotkin

(University of Edinburgh, UK)

Moggi proposed a monadic account of computational effects. He also
presented the computational lambda-calculus, lambda_{c}, a core
call-by-value functional programming language for effects; the effects are
obtained by adding appropriate operations. The question arises as to
whether one can give a corresponding treatment of operational semantics.

We do this in the case of algebraic effects where the operations are given
by a single-sorted algebraic signature, and their semantics is supported
by the monad, in a certain sense. We consider call-by-value PCF
with--and without--recursion, an extension of lambda_{c} with
arithmetic. We prove general adequacy theorems, and illustrate these with
two examples: nondeterminism and probabilistic nondeterminism.