Research

The Centre for Metacomputation aims to provide short-term funding for exploratory studies, leading to longer-term projects. Here are some examples of such studies, as well as ongoing projects:

Aspect Refactoring Tools

Refactoring is the automatic transformation of programs to improve their structure. Automatic refactoring tools are now included in all major development environments, such as Eclipse. However, writing refactoring tools is a time-consuming and error-prone task.

Aspect-oriented programming introduces new language features, in particular pointcuts, that interact with existing refactorings. The goal of the aspect refactoring project is to explore better formalisms for specifying refactorings, with the aim of producing refactorings for aspect-oriented languages.

Following a project with Torbjörn Ekman, the aspect refactoring project is currently explored under an EPSRC grant.

Efficient Data Structures for Streams in Haskell

In Haskell, the representation of sequences is considerably less efficient than in other languages (in particular for commonly used kinds of sequences, such as character strings). In return, the semantics of lists are highly convenient for programmers: lists are fully lazy, can be infinite or cyclic, and are simple to use.

Byte Strings are an efficient data structure for implementing strings in Haskell. Arbitrary Haskell programs can be adapted to use byte strings, for dramatic efficiency gains while retaining Haskell's declarative style.

Duncan Coutts, in collaboration with Roman Leshchinskiy and Don Stewart, is exploring representations of lists and functions on lists in Haskell, in particular leading to an improved notion of fusion, applicable to all list-like structures.

Game semantics, recursion schemes, and collapsible pushdown automata

Despite considerable progress over the past decade, the computer-aided verification of software remains a hugely challenging problem, for two main reasons: programs are infinite-state systems, and modern programs can only be accurately modelled using highly-structured mathematical models, as studied in semantics.

This project concerns an approach to software verification by developing automatic techniques which deal directly with infinite-state systems that are highly accurate models of programs. Following an initial study as part of the Centre for Metacomputation, Luke Ong is developing this project as a new EPSRC grant, together with Matthew Hague.

Flow Analysis and Higher-Order Programs

Flow analysis is the problem of statically approximating the flow of data and control in executions of a program. Many program analyses require flow analysis; and it is typically the case that more precise flow information leads to better analysis results.

It is difficult to give precise flow information for higher-order programs, due to the need to approximate higher-order calls. This is not a new problem, but existing methods often fail to yields precise enough results.

Damien Sereni and Luke Ong are currently exploring novel approaches to flow analysis in the higher-order case.

Further Information

The above is a short list of projects only. If you are interested in finding out more about the research interests of members, or are interested in collaborating with us, please visit our pages for more information.