We have developed correct, efficient algorithms for parsing general context free languages and modern computer hardware is sufficiently powerful to enable such techniques to be used.
I am interested in the application of these ideas to compiler code generation, specification of embedded systems, reverse compilation, natural language parsing and bioinformatics.
This work covers a broad spectrum, from graph theoretic algorithms for target code selection to meta-modelling of embedded systems.
Tools which implement the algorithms have been built and the work is brought together under Royal Holloway's
Centre for Software Language Engineering,
whose mission is to both enhance research in,
and facilitate the application of, software technologies that employ grammar based techniques.
The centre brings together academics and industrial users and aims to develop technologies which are both practical and correct.
I continue to be involved in work related to the PLanCompS project whose goal was to establish and test the practicality of a component-based framework for the design, specification and
implementation of programming languages. This was a large project, run jointly with Swansea University and with Microsoft Reseach as project partner, and it continues to be significant part of my current research focus.
My early research in Computer Science was in the area of formal methods and automated theorem proving, working on the general theory of well founded orderings in order to address the problem of proving process termination.
I have given a classification for the case of strings on two letters in terms of the order type of the ordering, and an automated proof of the correctness of a compiler as part of the ESPRIT PROCOS initiative.
My mathematical background is in infinite group theory, I constructed an example of a finitely presented simple group with unsolvable conjugacy problem.
I also published, jointly with Graham Higman, an OUP monograph on Existentially Closed Groups, which addresses an area on the borders between algebra and logic and uses algebraic techniques to prove results
which could not be derived using a purely logic based approach.