Differentiation in Deep Inference

As a member of the Mathematical Foundations group, my research will fall within the purview of proof theory and logic of computation. I will mainly be working with lambda calculus, my main supervisor's area of expertise. This is a model of computation in which terms can be interpreted as proofs or programs as per the Curry-Howard-Lambek correspondence. We gain a unique perspective on this by working within Open Deduction, a framework developed by Alessio Guglielmi, whom I will consult in his capacity as second supervisor.

The overall aim of this project will be to compare the notions of "differentiation" found in disparate areas of logic (type theory, lambda calculus, linear logic etc) as well as taking a more semantic approach to differentiation in lambda calculus, by combining recent developments made by my supervisors -for example in the representation of non-deterministic choice- with my own Analysis heavy mathematical training. Initially I am creating a notion of differentiation for lambda calculus in open deduction which I will then compare to The Differential Lambda Calculus proposed by Ehrhard et al (2001). I will also think about what integration may mean in this context. We hope that through this we will achieve a natural notion of substitution of proofs in open deduction.

This 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.