16/05/2002: Gordon Plotkin (LFCS, Univ. of Edinburgh)
Adequacy for Algebraic Effects.

Résumé

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 themselves are created and handled with the aid of additional {\em operations}.
The question arises as to whether one can give a corresponding general treatment of operational semantics. We do this in the case of {\em algebraic} operations, which may be infinitary (an alternative is to use {\em generic effects}). Algebraic operations seem to be precisely those which create effects.
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 examples: nondeterminism, probabilistic nondeterminism, interactive input/ouput, (global) state, and exceptions; certain difficulties remain in the last two cases.