About the Centre for Metacomputation

About Metacomputation

Metacomputation concerns the development of sophisticated computational tools for analysing the behaviour of programs. Such tools may operate at development time, for example to catch bugs, or they may operate at run-time, for instance to adapt the program to changing workloads. Techniques in metacomputation draw from a broad variety of different fields, including logic, automated theorem proving, compiler construction, program analysis, and software engineering. The time is ripe to unify these fragmented efforts in different communities and to help establish the emerging field of metacomputation and its foundations.

Examples abound where synergy between these different techniques has led to striking practical success. The SLAM project at Microsoft combines techniques from automated theorem proving (both model checking and deductive proof) as well as program analysis to locate many faults in device drivers. The Eclipse refactoring tools, developed at IBM, use a sophisticated system of type constraints to correctly implement refactoring transformations such as extract interface. Intel's Forte framework employs a functional programming language with reflection and metaprogramming features to get an effective framework for verification of industrial-scale hardware designs.

Foundational work in semantics has now reached a point where semantics can be seen, not simply as a mathematical tool for the analysis of programs, but as leading directly to computational representations and algorithmic methods. Model-checking can already be seen as a step in this direction. However, we see great additional potential in the use of compositional semantic methods in this context; in particular, in the analysis of open systems. Semantics endowed with a computational aspect is inherently metacomputational in nature, and many interesting new questions and possibilities arise. One the one hand, some new and very direct applications in program analysis can be envisaged. There are also some fascinating issues around reflection: can a program be the computational representation of its own semantics, and can such reflexivity be useful?

More broadly, we see a growing synergy between the semantics and program analysis community as greatly to the benefit of both, providing increased depth and formal rigour in program analysis, and new challenges and links to computational aspects in semantics.

The Project

The Centre is a four-year project funded by EPSRC. It is led by four senior academics of the Computing Laboratory.

The aim is to capitalise on synergies between these areas that have recently emerged in specific directions such as type systems for reflection, termination analysis, model checking of higher-order programs and the semantics of aspects. We plan to do so via a number of short-term pilot studies that - if successful - will give rise to further joint grant applications.

Members

The project is led by Samson Abramsky, Tom Melham, Oege de Moor and Luke Ong. Damien Sereni is the Research Associate for the project.

More information may be found on the members page.

Opportunities

We aim to conduct several short-term "pilot" studies to explore specific topics within metacomputation. The intention is that these projects, if successful, should lead to longer-term grants. If you are interested in postdoc opportunities to work on such projects please contact us.