I'm a Lecturer and Prize Fellow in the Mathematical Foundations group, Department of Computer Science, University of Bath.
My research is in the area of logic and proof theory, and has focused on canonical graphical representations of proof, commonly known as proof nets.
We give an effective correctness criterion for additive proof nets, which is naturally expressed in Petri nets, and is the equivalent of Danos contractibility for MLL. In addition we give simple proof search algorithms for additive linear logic with and without units and an effective correctness algorithm for additive proof nets with units, and we show that first-order additive linear logic is NP-complete.
We consider a notion of semi-star-autonomous category: star-autonomous categories without units, corresponding to Girard's proof nets for MLL.
Proof equivalence in MLL with units is shown to be PSPACE-complete, by a reduction from the graphical formalism called Non-Deterministic Constraint Logic. This effectively rules out a satisfactory notion of proof net with units, as such a notion would constitute a tractable decision algorithm for proof equivalence.
The atomic lambda-calculus is a typeable lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait's reducibility method.
The atomic lambda-calculus is a typeable lambda-calculus with explicit sharing, based on a Curry-Howard-style interpretation of the deep inference proof formalism. Duplication of subterms during reduction proceeds `atomically', i.e. on individual constructors, similar to optimal graph reduction in the style of Lamping. The calculus preserves strong normalisation and achieves fully lazy sharing.
The paper describes canonical proof nets for additive linear logic, or sum-product logic, the internal language of categories with free finite products and co-products. Starting from existing proof nets, which disregard the unit laws, canonical nets are obtained by a simple rewriting algorithm, for which a substantial correctness proof is provided.
Awarded the LICS 2011 Kleene award for best student paper
The paper investigates cut-elimination in classical proof forests, a proof formalism for first-order classical logic based on Herbrand's Theorem and backtracking games in the style of Coquand. Cut-free classical proof forests were described by Miller, and are called Expansion Tree Proofs.
Superseded by Classical Proof Forestry.
Laboratory for the Foundations of Computer Science (LFCS) School of Informatics | University of Edinburgh
Doctoral thesis: Graphical Representation of Canonical Proof: Two case studies
Thesis advisor: Professor Alex Simpson
Department of Philosophy | Utrecht University
Winner of the Cognitive Artificial Intelligence thesis award 2007, Department of Philosophy, Utrecht University
Department of Computer Science 1 West 4.67 Claverton Down Bath BA2 7AY United Kingdom email@example.com