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.

PhDs

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

Research

Our research interests are:

• Category theory (Power, Wingfield)
• Computer algebra (Bradford, Davenport, England, Evans, Jones, Locatelli, Wilson)
• Cryptography (Davenport, Kaafarani)
• Geometry (Hameed, Vorobjov)
• Proof theory (Bruscoli, Das, Guglielmi, Heijltjes)
• Semantics (Heijltjes, Laird, McCusker)

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

Guy McCusker analyses 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 his 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.

Willem Heijltjes' work investigates the nature of formal proof, in search of geometric representations that capture its essence. Such objects, often called `proof nets´, enable a deep understanding of logic, of fundamental structures in category theory and of the foundational aspects of computation.

Jim Laird constructs mathematical models of programming languages which capture precise behavioural properties of programs, like control and information flow, or resource usage. He then investigates the algebraic structure of these models to recover new ways of writing programs and new theories for reasoning about them.

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.