Centre for Metacomputation

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.