Foundations of Computation
Research concerns the mathematical foundations of computer science. The topics we are interested in include algorithms, computational complexity and combinatorics, logical methods, program semantics, hardware and software verification and interactive theorem proving.
Our research advances the theory of computer science, its mathematical and conceptual foundations. It ranges from the design and analysis of algorithms and the study of computational complexity to the development of models for programs, networks, hardware and software systems, and of tools for analysing them.
Computing systems are arguably the most complex technologies humans have built. Our work helps understanding them and making them more efficient, sustainable and trustworthy and our research is driven by fundamental questions about the nature of computation as well as the need for rigorous mathematical foundations for real-world applications.
Research highlights
New tool for optimisation problems on typical networks
We have developed a new tool for describing solutions to optimisation problems on large random networks, which can be applied to key problems such as Maximum Cut and the Alignment Problem - a quantitative version of the Isomorphism Problem.
Both are canonical computational challenges, and our technology not only provides approximate solutions but also reveals their topological properties.
Who’s Guarding the Guardians: Foundations of Formal Reasoning
Tools specialized in the formal verification of software and hardware are a celebrated application of mathematical logic to computer science. Isabelle/HOL is a popular such tool, which has been successfully used by researchers from the Sheffield FOX group to build verification frameworks for hybrid systems and establish information flow security of hardware optimizations.
The verification tools, while guardians of system correctness, themselves require solid (inconsistency free) logical foundations, including powerful reasoning principles. Our research on the foundations and recursive specification mechanisms of Higher-Order Logic has found applications to provers such as Isabelle/HOL, leading to a breakthrough in verification technology – in a line of work that has been well received by the programming language community.