# Structural Operational Semantics for Computational Effects

## John Power

(Bath)

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