## Towards more refined notions of computation: the global state example

School of Informatics

University of Edinburgh

Thursday, 20 December 2012, 11:00 (note the unusual time)

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: In seminal work, Moggi proposed the use of strong
monads to model copmutational effects (so-called notions of
computations) in programming languages. Later, Plotkin and Power
showed that a wide range computational effects can be identified with
algebraic theories whose free algebras determine the monads proposed
by Moggi.

This talk is about the first steps in our work of investigating
more refined notions of computation by studying the combination of
refinement types and algebraic theories of computational effects.

I will give a brief overview of algebraic theories of computational
effects and refinement types before showing a small motivating example
of global state where every location can be switched on and off (and
also equipped with specific permission requirements). This example
illustrates step-by-step the generalizations we have made to the
conventional algebraic theories and also indicates how the general
notion of algebra, we are after, might look.

(Joint work with Gordon Plotkin and Alex Simpson.)

Tarmo Uustalu

Last update 20.12.2012