Categorical Semantics and Deep Inference

I am interested in the foundations of computing, specifically proof theory and proof complexity and for my PhD I wish to investigate structural proof theory. I am interested in 'Deep Inference' whose investigators includes one of my supervisor Alessio Guglielmi, and the search for an efficient and natural proof system. This project came from the fundamental question 'What is a proof?' and 'When are two proofs the same?'. I am also interested in understanding normalisation of proofs, an area that has important and deep connections with computer science, and the Curry-Howard-Lambek correspondence between programming language theory, proof theory and category theory. I hope to investigate how developments in proof theory due to deep inference relate to categories through this correspondence. The research will likely span a range of EPSRC research areas, possibly including but not necessarily limited to: Algebra, Architectures and Operating Systems, Complexity Science, Geometry and Topology, Logic and Combinatorics, Maths of Computing, Theory of Computation, and Verification and Correctness.