Structure vs. Invariants in Proofs (StrIP)

All numbers are even or odd. But why? How could I prove this *formally*? One way is to notice that the parity of a number flips every time we add 1, another way is to just check the last digit. Both of these 'proofs' induce an 'algorithm' for checking whether a number is even or odd. However in the latter case the algorithm is exponentially more efficient, - we only need to look at one digit rather than generate the entire number from scratch. In this way we can say that the two proofs are really *different*.

'Structure vs. Invariants in Proofs' (StrIP), at its most abstract level, is concerned with understanding when two proofs are different or the same. This is a question in proof theory that can be traced back to the early 20th century, and is often known as Hilbert's 24th problem. While it is a fundamentally theoretical question, Hilbert's 24th problem and the proof theoretic endeavours that have followed underlie many aspects of modern computer science, such as programming language theory and computability theory. In particular, proof theory is one of the foundational pillars of Formal Verification. This is an emerging field that allows us to often *guarantee* that software functions correctly, and is set to become increasingly relevant for certifying software in the real world.

However, there remains one fundamental barrier to resolving Hilbert's 24th problem: inductive reasoning. 'Induction' is a powerful proof technique that is indispensable in mathematics and computer science; it allows us to prove a property P(x) for all numbers x by first proving P(0) then proving that P(x) always implies P(x+1). It is like an infinite sequence of dominoes: if I knock over the first one, every other one will eventually fall. On the computing side, a proof theoretic treatment of induction is a necessity in order to reason about general computer programs.

The goal of StrIP is to give a comprehensive treatment of induction via the notion of 'cyclic proofs'. This is a phenomenon that has emerged in computational logic over the last 20-30 years and allows us to decompose induction into finer computational steps in a finitary way. By combining this with other recent ideas in proof theory, so-called 'Deep Inference', StrIP will build a bridge between two of the most important subjects in theoretical computer science: proof theory and automata theory. Ultimately, the goal is to apply the techniques developed to Automated Reasoning via concrete implementations, and more generally to the automated verification of computer programs.

This fellowship (StrIP) is primarily based in theoretical research, and thus will have principal short-medium term impact on academia and, at a national level, the wider research community. StrIP will advance the state of the art in theoretical computer science, and thus accelerate the general progression of computing industries in the long term.

In particular, StrIP will benefit the software industry, especially in the UK, thanks to the development of techniques that may be applied to Automated Reasoning and programming language theory. More generally, StrIP contributes to the area of Formal Verification, which increasingly affords us the ability to certify the correctness of software in practice. This will have a positive impact on technological innovation in the long term, and thus for the economy too.

In the short term, within the duration of StrIP, I will engage with the wider UK public in the form of outreach events. This may include popular science events, open days or visits to local schools. In particular, I aim to contribute to the public understanding of Formal Verification as a way to build trust in software that we rely on.