EPSRC logo

Details of Grant 

EPSRC Reference: EP/D037085/1
Title: Centre for Metacomputation
Principal Investigator: Abramsky, Professor S
Other Investigators:
Ong, Professor CHL De Moor, Professor O Melham, Professor T
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: Platform Grants (Pre-FEC)
Starts: 01 March 2006 Ends: 28 February 2010 Value (£): 431,107
EPSRC Research Topic Classifications:
Fundamentals of Computing Modelling & simul. of IT sys.
Software Engineering System on Chip
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:  
Summary on Grant Application Form
Metacomputation concerns the development of sophisticatedcomputational tools for analysing the behaviour of programs. Suchtools may operate at development time, for example to catch bugs, orthey may operate at run-time, for instance to adapt the program tochanging workloads. Techniques in metacomputation draw from a broadvariety of different fields, including logic, automated theoremproving, compiler construction, program analysis, and softwareengineering. The time is ripe to unify these fragmented efforts indifferent communities and to help establish the emerging field ofmetacomputation and its foundations. To do so is the primary objectiveof this proposal.Examples abound where synergy between these different techniques hasled to striking practical success. The SLAM project at Microsoftcombines techniques from automated theorem proving (both modelchecking and deductive proof) as well as program analysis to locatemany faults in device drivers. The Eclipse refactoring tools,developed at IBM, use a sophisticated system of type constraints tocorrectly implement refactoring transformations such as extractinterface. Intel's Forte framework employs a functional programminglanguage with reflection and metaprogramming features to get aneffective framework for verification of industrial-scale hardwaredesigns.Foundational work in semantics has now reached a point where semanticscan be seen, not simply as a mathematical tool for the analysis ofprograms, but as leading directly to computational representations andalgorithmic methods. Model-checking can already be seen as a step inthis direction. However, we see great additional potential in the useof compositional semantic methods in this context; in particular, inthe analysis of open systems. Semantics endowed with a computationalaspect is inherently metacomputational in nature, and many interestingnew questions and possibilities arise. One the one hand, some new andvery direct applications in program analysis can be envisaged. Thereare also some fascinating issues around reflection: can a program bethe computational representation of its own semantics, and can suchreflexivity be useful?More broadly, we see a growing synergy between the semantics andprogram analysis community as greatly to the benefit of both,providing increased depth and formal rigour in program analysis, andnew challenges and links to computational aspects in semantics.
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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