Department of Computer Science

Group members

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.

Proof formalism for first-order classical logic based on Herbrand\'s Theorem and backtracking games in the style of Coquand - Two diagrams related by an arrow. each diagram contains logical symbols and letters representing variables and terms.

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.

PhDs

There are opportunities for postgraduate research in our group. Please contact academic staff directly if their area of research interests you.

ResearchAbstract proof representation - On the left of an arrow, two diagrams representing bifurcations and related by a slash symbol; on the right of the arrow, one of the diagrams is inserted into the other in two different ways, which are related by an equal sign.

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

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.

Cryptography

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.

Semantics

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.

Proof theory

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 are a founding member of the Wessex Theory Seminar, funded by the London Mathematical Society. We also regularly run the Mathematical Foundations Seminar and the Triangular Seminar.

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.