Semantic approaches to control of interference in higher-order imperative languages

Back to my home page.

View my research papers.

View my research projects.

Project description

EPSRC grant GR/N22014, value £58359, running June 2000-May 2003.

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, and enjoyed the collaboration of Matthew Wall and Dan Ghica.

Project outcomes

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

• The subject of algorithmic game semantics was initiated by research supported by this grant. Some papers and talk slides are below.

  Dan R. Ghica and Guy McCusker. The regular language semantics of second-order Idealised Algol. To appear in Theoretical Computer Science, 2003. Available as postscript and PDF, gzipped.

  Guy McCusker. Game Semantics of Imperative Languages using Regular Expressions. Slides from the Spring School on Theoretical Computer Science 2002, Agay, France.

  • The first lecture is an overview of game semantics
  • The second lecture covers the regular language presentation.

  The slides are PDF files.

  Dan R. Ghica and Guy McCusker. Reasoning about Idealised Algol using regular languages. In Proceedings, Twenty-Seventh International Colloquium on Automata, Languages and Programming (ICALP 2000). Available as postscript.

• We discovered that Reddy's model of SCI is fully abstract, and that it can be presented using monoids and relations.

  Guy McCusker. A graph model for imperative computation. Slides for my invited lecture at CTCS 2002. Available as PDF.

  Guy McCusker. A fully abstract relational model of Syntactic Control of Interference. In Proceedings, Computer Science Logic (CSL) 2002, volume 2471 of LNCS, copyright © 2002 Springer-Verlag.

  • Paper available as PDF.
  • Slides from my talk available as PDF.

• We developed fully abstract games models of SCI and SCIR (McCusker, Wall). Some articles describing this work are currently being prepared.
• A notion of categorical model for SCIR, with coherence proof, was developed (McCusker). Notes on this will appear here soon.
• A decomposition of SCI in terms of sequoidal logic was found (Laird). Notes on this will appear here soon.