New foundations of proof theory from a novel notion of substitution

我的研究将在证据理论领域，为当前开发证据替代概念的努力做出贡献。作为计算组的数学基础的一员，我的工作也可能涉及范畴论和计算理论，因为证明可以通过Curry-Howard-Lambek对应被解释为程序。我的项目将特别关注结构证明理论，特别是深度推理，这是由我的导师Alessio Guglielmi开发的证明系统的设计方法。深度推理旨在减少证明中不必要的句法官僚主义，只保留必要的语义信息。我的工作将有助于目前的努力，发展一个概念的替代证明在深推理，这应该使一个强大的形式的证明因式分解。这可能会对证明理论中的一系列问题产生影响，包括证明规范化和证明的同一性，以及对证明复杂性的影响。我的工作可能会跨越EPSRC的一系列研究领域，可能包括但不一定限于：代数，复杂性科学，几何和拓扑学，逻辑和组合学，编程语言和编程器，理论计算机科学，验证和正确性。

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.