Personal tools
You are here: Home Events Abstract Archives 2007-2008 Structural Operational Semantics for Computational Effects

Structural Operational Semantics for Computational Effects

John Power LFCS 3pm Tuesday 25th September 2007 Room 2511, JCMB, King's Buildings Note nonstandard time! This is a special seminar to celebrate John's 18 years at LFCS, since he is moving to Bath at the end of September. The seminar will be followed by a leaving party for John in room 2510

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)

Document Actions