Unified Semantics of Hybrid Computational Effects

Back to my home page.

View my research papers.

View my research projects.

Project description

EPSRC grant GR/N38824, value £177,943, running January 2001-October 2003.

Modern programming languages provide powerful mechanisms for manipulating state, via assignment statements, and control flow, via goto statements, exceptions and continuations. These computational effects are often exploited in combination, and some constructs such as exceptions are in fact hybrids: mixed state/control effects.

To date, no satisfactory semantic models of combined or hybrid effects exist. However, recent advances in the field of game semantics suggest that games provide a suitable universe in which an appealing denotational account of combined and hybrid effects can be given.

In this project, we will use the technology of game semantics to produce such an account. We will first study combined effects by generalizing and extending existing work on games, and then use this extended semantic space to study hybrid effects, particularly exceptions and coroutines. This will provide the first accurate denotational models of these features. A second strand of work will analyse the games universe directly with a view to discovering a logic for manipulating the strategies used to interpret programs. Finally and most ambitiously, we will develop a theory of computational effects which predicts and classifies the range of behaviours available to programs, and establish metatheorems about these generalized effects.

This project employed Russell Harmer from January 2001 to March 2002, and Jim Laird from January 2001 to February 2003, and June 2003 to September 2003.

Project outcomes

The final report on the project describes the research outcomes of the work carried out with this EPSRC support.

Links to the papers produced as part of this project will appear here soon.