On this page you can find some information about the research grants which I hold or have held. Most of this is just blurb taken from the grant application forms.

An £11950 International Joint Research Project funded by the Royal Society to support collaboration between the Bath MathFound group and Pino Rosolini's group at Genova.

We aim to give a unified mathematical account of the semantics of programming in a number of styles: higher-order functional programming; imperative programming; and logic-programming. In recent years, several developments in the field of semantics have independently made use of very similar mathematics to provide models for these various styles of programming. We will study these models, analyse what they have in common, provide a unified setting for them, and investigate how reasoning and programming principles may be transferred from one style to another via the commonalities embodied in the models.

A small grant (£1400 per year) from the London Mathematical Society supports joint seminars between research groups at Bath, Southampton, Oxford, Swansea, Imperial, Queen Mary, Cambridge and Sussex. Full details of the activity of the Wessex seminar can be found on the Wessex wiki.

This is a British Council Prime-Minister's Initiative (PMI2) collaboration grant between our group at Bath and the Centre for Verification and Semantics at AIST, Japan; valued at £39803, it ran for two years from May 2008.

See our PMI2 wiki page for full details of the activity of the project.

EPSRC grant GR/S72181/01, value £165874, running November
2004-September 2007. Rated *outstanding* at the final EPSRC
review.

Game semantics is a way of modelling programming languages intensionally: in a games model, a program is interpreted by a sequence of interactions which it may have with its environment. Domain theory, on the other hand, models programs extensionally, using functions between certain structured sets.

Games have been very successful in recent years at modelling a wide variety of programming languages with a range of sophisticated features such as state and control operators. The remarkable feature of these models is that they are very precise: there is an absolute correspondence between properties in the model and properties in the language. On the other hand, while domain theoretic models are seldom so precise , they have proved successful in the sense that they are easy to work with and enjoy a rich mathematical theory.

Recent developments in domain theory (Laird's notion of bistability) suggest that close connections between game semantics and domain-based semantics are available. This project seeks to discover and elaborate these connections: we will investigate how the intensional modelling of game semantics can be carried out in a domain-theoretic setting, and how the various different kinds of domains correspond to new kinds of games. The outcomes will be a range of new models of programming languages , and techniques for constructing such models, as well as a theory connecting games to domains.

The goal of this project is to develop a rich semantic theory for modelling programming languages, based on game semantics, domain theory and the connections between them. Specifically, we aim

- to import the insights of game semantics into domain theory, to develop extensional models with a game-like intensional character. This should lead to fully abstract domain theoretic models of programming languages incorporating state, local control, nondeterminism and concurrency.
- in the other direction, to discover games models corresponding to different kinds of domain, leading to fully abstract and effectively presentable models of the lazy lambda-calculus and functional languages with nondeterminism.
- to analyze the common structure of the domain and game-theoretic models, and extract a range of techniques for constructing and reasoning about such models, and hence about the programming languages they model.

This project employed Jim Laird and many of its outputs are available from his web pages.

There is also a final report page for this project.

EPSRC grant GR/N22014, value £58359, running June 2000-May
2003. Rated *tending to outstanding* at the final EPSRC
review.

The aim of this project is to produce a precise semantic model of interference and interference-control in higher-order programming languages with references. This should be taken to include object-oriented languages as well as languages such as ML. The model will be used to discover and support new reasoning principles and type systems for taming interference. Specific goals are to develop and analyse games models for existing interference control systems, to develop new systems or other mechanisms for controlling interference, and to construct proof systems and reasoning principles for proving the correctness of programs in the presence of interference control.

This project employed Jim Laird as a research fellow from June-December 2000 and March-May 2003.

Some papers on models of interference controlled languages can be found here.

There is also a final report page for this project.

EPSRC grant GR/N38824, value £177,943, running January
2001-October 2003. Rated *tending to outstanding* at the final EPSRC
review.

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 employs Jim Laird from January 2001.

There is also a final report page for this project.