Towards more refined notions of computation: the global state example

Danel Ahman

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.)

ERDF
Tarmo Uustalu
Last update 20.12.2012