Gordon Plotkin (Edinburgh University, LFCS)

Concurrency and the Algebraic Theory of Effects

The algebraic theory of effects continues Moggi’s monadic approach to effects by concentrating on a particular class of monads: those that can be given by equational theories. Their operations can be thought of as effect constructors, as it is they that give rise to effects. Examples include exceptions (when the theory is that of a set of constants with no axioms), nondeterminism (when the theory could be that of a semilattice, for choice, with a zero, for deadlock), and action (when the theory could be a set of unary operations with no axioms). Two natural, apparently unrelated, questions arise: how can exception handlers and concurrency be incorporated into this picture? For the first, in previous work with Pretnar, we showed how free algebras give rise to a natural notion of computation handling, generalising Benton and Kennedy’s exception handling construct. This can be thought of as an account of (unary) effect deconstructors.

Turning to, for example, CCS, the evident theory, at least for strong bisimulation, is that of nondeterminism plus action. Then restriction and relabelling are straightforwardly dealt with as unary deconstructors. In order to deal with concurrency, we give a theory of binary deconstructors. It applies to CCS and other process calculi, as well as to shared memory parallelism. In this way we demonstrate a possibility: that the monadic approach (which has always accounted for resumption semantics) can be fruitfully integrated with the world of concurrency.