New foundations of proof theory from a novel notion of substitution

My research will be in the area of proof theory, contributing towards current efforts to develop a notion of substitution of proofs. As a member of the Mathematical Foundations of Computation group, my work may also touch on category theory and the theory of computation since proofs may be interpreted as programs via the Curry-Howard-Lambek correspondence.

My project will focus specifically on structural proof theory, in particular deep inference, a design methodology for proof systems developed by my supervisor Alessio Guglielmi. Deep inference seeks to reduce the unnecessary syntactic bureaucracy in proofs and retain only the necessary semantic information. My work will contribute to current efforts towards developing a notion of substitution for proofs in deep inference, which should enable a powerful form of proof factorization. This is likely to have impact on a range of problems in proof theory including proof normalization and identity of proofs, as well as having an impact on proof complexity.

My work will likely span a range of EPSRC research areas, possibly including, but not necessarily limited to: Algebra, Complexity Science, Geometry and Topology, Logic and Combinatorics, Programming Languages and Compilers, Theoretical Computer Science, and Verification and Correctness.