Structural Operational Semantics for Computational Effects

John Power


In seeking a unified study of computational effects, a fundamental task
is to give a unified structural operational semantics, together with an
adequate denotational semantics for it, in such a way that, for the
leading examples of computational effects, the general definitions are
consistent with the usual operational semantics for the relevant
effects. One can readily produce a unified operational semantics that
works fine for examples that include various forms of nondeterminism
and probabilistic nondeterminism. But that simple semantics fails to
yield a sensible result in the vitally important case of state or
variants of state. The problem is that one must take serious account of
coalgebraic structure. I shall not formally enunciate a general
operational semantics and adequacy theorem in this talk, but I shall
explain the category theory that supports such a semantics and theorem.
I shall investigate, describe, and characterise a kind of tensor of a
model and a comodel of a countable Lawvere theory, calculating it in
leading examples, primarily involving state. Ultimately, this research
supports a distinction between what one might call coalgebraic effects,
such as state, and algebraic effects, such as nondeterminism.

(Joint work with Gordon Plotkin)

Thursday 13th November 2008, 14:00
Robert Recorde Room
Department of Computer Science