Topological and graphical interpretations of proofs

My research will focus on proof theory and the search for an efficient and natural formalism. We would like to develop a representation of proofs which would retain only the semantic information necessary for normalisation while discarding the unnecessary syntactic bureaucracy. This will allow us to find normal forms for proofs, which will then enable us to answer the question of what it is for two proofs to be the same. Proof theory is related via the Curry-Howard-Lambek correspondence to categories and the theory of computation, and so normalisation procedures for proofs can be given a direct computational interpretation and can be informed by categorical considerations.
I intend to work with graphical and topological representations of proofs, which can then be manipulated in an intuitive way to give normalisation procedures. I will do this using the deep inference framework developed by my supervisor Alessio Guglielmi, which restores the vertical symmetry of proofs and allows inference at any depth of a formula, allowing for more natural manipulation of proofs. I will also use logical flow methods such as atomic flows, proof nets, and combinatorial proofs, which are areas of expertise for my supervisors Alessio Guglielmi and Willem Heijltjes.
The research 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.