Details of Grant 

EPSRC Reference:	GR/R88861/01
Title:	Algorithmic game semantics and its applications
Principal Investigator:	Abramsky, Professor S
Other Investigators:	Ong, Professor CHL
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Oxford
Scheme:	Standard Research (Pre-FEC)
Starts:	01 May 2002	Ends:	31 October 2005	Value (£):	319,022
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Game Semantics has emerged as a powerful paradigm for giving semantics to a variety of programming languages and logical systems. This project aims to develop Game Semantics in a new, algorithmic direction, with a view to applications in computer-assisted verification and program analysis. Game Semantics provides a very concrete way of building fully abstract models. It has a clear operational content, while admitting compositional methods in the style of denotational semantics. The promise of this approach is to carry over the methods of model checking based on automata-theoretic representations, which has been so effective in the analysis of circuit designs and communications protocols, to much more structured programming situtations, in which data-types and control flow are important. Our aim is to build on the tools and methods which have been developed in the verification community, while exploring the advantages offered by our semantics-based approach. The research programme is founded on new automata-theoretic characterizations of the fully abstract game model of significant fragments (up to 3 order, including Iteration) of Idealized Algol (IA) - a variant of Core ML, and algorithms for deciding observational equivalence for these fragments. We seek to extend the automata-theoretic representations to richer language features (e.g. control, non-determinism and probability), higher-order programs and recursion, and develop applications in the model checking of behavioural properties of imperative languages with local variables and procedures.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ox.ac.uk