- Andrea Aler Tubella
- Can Baskent (personal page)
- Valentin Blot (personal page)
- Russell Bradford (personal page)
- Paola Bruscoli (personal page)
- James Davenport (personal page)
- Etienne Duchesne
- Matthew England (personal page)
- Ieuan Evans (personal page)
- William John Gowers
- Alessio Guglielmi (personal page)
- Mesar Hameed (personal page)
- Fanny He
- Willem Heijltjes (personal page)
- Jessica Jones (personal page)
- Jim Laird (personal page)
- Acyr Locatelli (personal page)
- Guy McCusker (personal page)
- John Power
- Benjamin Pring (personal page)
- Benjamin Ralph
- Alessio Santamaria
- Daniel Schmitter
- David Sherratt
- Nicolai Vorobjov (personal page)
- David Wilson (personal page)
Former group members
Mathematical foundations of computation
Our group explores the two-way relationship between mathematics and computer science.
We use computers to manipulate representations of algebraic and geometric concepts, with applications to topics such as cryptography, security and engineering. We are the UK's leading centre for this work in computational mathematics and its applications. We are the EU centre of expertise on interfacing computer algebra to numeric calculations.
At the same time, we use mathematical structures to put computer science on firm theoretical foundations. We are concerned with the mathematical understanding of logical reasoning, of programs, of processes, of programming languages, and of theorem provers. Our methods include ideas and techniques from category theory, game theory, model theory, proof theory and type theory, as well from more traditionally computational topics such as automata, formal languages and computability.
There are opportunities for postgraduate research in our group. Please contact academic staff directly if their area of research interests you.
Our research interests are:
- Category theory (Duchesne, Laird, McCusker, Power, Schmitter)
- Computer algebra (Bradford, Davenport, England, Evans, Jones, Locatelli, Wilson)
- Cryptography (Davenport, Kaafarani, Pring)
- Geometry (Hameed, Vorobjov)
- Proof theory (Aler Tubella, Blot, Bruscoli, Duchesne, Guglielmi, He, Heijltjes, Ralph)
- Semantics (Blot, Duchesne, He, Heijltjes, Laird, McCusker, Ralph)
Category theory arose from Algebraic Topology in the 1940's; it acquired independent status early in the 1960's, when it was used to characterise Universal Algebra, equivalently equational theories in logic. Soon afterwards, and in connection with logic, it began to be used in theoretical computer science, in particular in regard to semantics of programming languages, which are used for specification and verification.
Work in cryptography has included James Davenport's contribution to breaking the US Federal Reserve Bank encryption method for bank-bank communication in the USA, made possible by new Computer Algebra software he had been working on.
We analyse programs, programming languages, logic and proofs using mathematical models. Developing models of programs reveals their structure and can result in new approaches for analysing their behaviour. Most of this work involves game semantics, in which programs or proofs are modelled as strategies for certain kinds of games, and changing the features of a programming language amounts to changing the rules of the game.
We also build mathematical models of programming languages which capture precise behavioural properties of programs, like control and information flow, or resource usage. We then investigate the algebraic structure of these models to recover new ways of writing programs and new theories for reasoning about them.
We are interested in the logical foundations of computing and in the relation between proof theory and computation. Our aim is to establish and strengthen such a relation to a point where each field can benefit from the techniques developed for the other.
One of the tools we use is a theory called `deep inference´, which, among other things, introduces powerful geometric methods into proof theory. Another tool is category theory, which allows us to study the semantics of proofs and tackle century-old problems such as that of deciding when two proofs or two algorithms are the same.
The group environment
We have scientific relations with many international institutions, including:
AIST Amagasaki site, Kansai (Japan); Hewlett Packard; Imperial College; Joint INRIA/Microsoft Research Centre; Laboratoire LIX (INRIA, École Polytechnique), Palaiseau (France); Laboratoire LORIA (INRIA Nancy-Grand Est), Nancy (France); Laboratoire PPS (CNRS, Paris 7), Paris; Macquarie University; MapleSoft; Queen Mary, University of London; RISC (University of Linz); Swansea University; Technische Universität Dresden (Germany); Technische Universität Wien (Austria); Università di Torino.; Universities of Waterloo and Western Ontario; University of Birmingham; University of Cambridge; University of Dundee; University of Edinburgh; University of Genoa (Italy); University of Helsinki; University of Leicester; University of Oxford; University of Southampton; University of Strathclyde; University of Sussex; University of Timisoara; University Politehnica of Bucharest.