I am a Senior Lecturer in the Programming Languages Group in the School of Computer Science at the University of Bristol. My work concerns 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, accessible introduction to my POPL'24 work on a fundamental new extension to the notion of type system, and an application to incorrectness reasoning.
 Intensional Datatype Refinement : a short, accessible 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 more accessible introduction to my POPL'23 work on a decidable fragment of higherorder Horn clauses and a deeper 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. A $50k 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
 Toby Cathcart Burn, cosupervised with Luke Ong and funded by the University of Oxford.
 Eddie Jones, cosupervised with Luke Ong and funded by the VeTSS Research Institute.
 Charlie Walpole, funded by the University of Bristol.
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.