My research interests include (but are not limited to) the following topics.

  • Formal verification
  • Refactoring and program synthesis
  • Semantics
  • Logic and proof theory
  • Inductive and coinductive reasoning
  • Metaprogramming and intensional computation
  • Type systems and computational models

Some things I have worked on include the following. See my publications and software pages for more details.

Trustworthy Refactoring for OCaml

Whilst at the University of Kent, I worked on the ‘Trustworthy Refactoring’ project (EPSRC Grant EP/N028759/1) with Simon Thompson, Scott Owens, and Hugo Férée. The aim of this project was to develop a framework in which refactorings for the OCaml programming language can be formally specified, and verified to be behaviour preserving. We developed a prototype tool called ROTOR, and an abstract static semantics for a subset of OCaml that formalises our approach.

Cyclic Proof and Program Verification

I work on aspects of proof theory, specifically a notion of proof which allows derivations of infinite height but with a well-formedness condition that guarantees soundness. This essentially encodes forms of inductive reasoning. A natural finite representation of infinite proofs is using finite derivation trees with cycles, hence the term “cyclic” proof. I have investigated the theory of non-wellfounded and cyclic proofs in different contexts, including first order logic, Herbrand logics, and modal logics.

I worked with James Brotherston at University College London on investigating how to expand verification techniques making use of separation logic and cyclic proofs. This project (funded by EPSRC Grant EP/K040049/1) focused on the development of the Cyclist theorem proving framework. My work in particular added capabilities for proving termination of procedural code with recursion.

Abductive Programming for Machine Learning

With colleagues at the University of Birmingham, I implemented an abductive calculus for machine learning as a PPX extension to OCaml. This represents a new, principled paradigm for programming machine learning. It is based on the observation that the process of learning the parameters of a model can be seen as an analogue of C. S. Peirce’s logical principle of abduction. The calculus allows models to be defined using the functional programming paradigm and their tunable parameters, denoted by provisional constants, to be handled implicitly in a clean way.

Factorisation Calculus

The Factorisation Calculus is a combinatory rewrite system with the capability to analyse the syntactic structure of a wide class of its own terms, making it a good candidate for a fundamental model in which to study intensional computation, reflection, and meta-programming. I have described an encoding of the Factorisation Calculus into the λ-Calculus; I also supervised an MEng dissertation looking at a structural type system for the Factorisation Calculus.

Intersection Types for Featherweight Java

In my MSc Dissertation and PhD Thesis I investigated intersection type assignment for Featherweight Java, under the supervision of Steffen van Bakel. Intersection types are a type-theoretic approach for ad-hoc polymorphism, allowing to specify that an expression has a particular number of different types all at once. This allows an exact type-based analysis, even with recursion, since each expression can be given a type for each time it is used. Featherweight Java is a formal calculus modelling the core features of class-based object-oriented programming. I defined an intersection-based type system for it, and showed that this can be used as a basis for a denotational semantics. I also looked at type inference for Nakano’s guarded recursion.

Recursive Adaptive Grammars

An older research interest, which has been on the back burner for a while, is in frameworks for extensible programming languages, and recursive adaptive grammars (RAGs) in particular. I have written a RAG-based parser in Java which is hosted on Sourceforge. (I really should move this over to Github, or similar!)