I am a Senior Lecturer in the Programming Languages Group in the School of Computer Science at the University of Bristol. I work on mathematical theories for reasoning about computation, and their application in the design of more intelligent and predictable tools for programming.
If you are interested in studying for a PhD with me on one of these topics, take a look at my research below and then let me know what you are interested in. For some of my more recent papers, I have linked separate introductions that are more suitable for a general PL audience (some background in type systems and/or logic).
Research
My research is on program analysis and automated reasoning, especially for applications in program verification.

Tools for functional programming [POPL'21] [PLDI'22] [POPL'24]. Designing tools based on automated reasoning to help programmers write bugfree code.
 IllTyped Programs Don't Evaluate : a short introduction to my POPL'24 work on a new extension to the notion of type system, and an application to incorrectness reasoning.
 Intensional Datatype Refinement : a short introduction to my POPL'21 work on a refinement type system for predictable program analysis for verifying (patternmatch) safety properties.

Fragments of higherorder logic [POPL'18] [LICS'21] [POPL'23]. Investigating restrictions of higherorder logic that give good computational properties.
 HigherOrder MSL Horn Constraints : a short introduction to my POPL'23 work on a decidable fragment of higherorder Horn clauses and a semantic correspondence between formulas and types.
 Higherorder model checking [POPL'11] [POPL'14]. Designing new methods for the higherorder extension of software model checking.
 Automata over infinite alphabets [LICS'15] [JCSS'17]. Classifying foundational problems for register automata by their computational complexity.
Funded Projects
 Meta Research. An award to develop a scalable static taint analysis for Core Erlang.
 EPSRC (EP/T006595/1). A 3.5 year project on HigherOrder Constrained Horn Clauses: A New Approach to Verifying HigherOrder Programs.
 UK Research Institute on Verified, Trustworthy Software Systems. A PhD studentship on HigherOrder Program Invariants.
PhD Students
 Charlie Walpole, funded by the University of Bristol.
 Eddie Jones, funded by the VeTSS Research Institute.
Teaching
I run the following two courses at the University of Bristol:
 COMS30040: Types and Lambda Calculus. An introduction to the theory of PCF, pure lambda calculus and the CurryHoward correspondence.
 COMS20007: Programming Languages and Computation. An introduction to programming language theory and the theory of computation.