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 bug-free code.
  
  • Ill-Typed 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 (pattern-match) safety properties.
• Fragments of higher-order logic [POPL'18] [LICS'21] [POPL'23]. Investigating restrictions of higher-order logic that give good computational properties.
  
  • Higher-Order MSL Horn Constraints : a short introduction to my POPL'23 work on a decidable fragment of higher-order Horn clauses and a semantic correspondence between formulas and types.
• Higher-order model checking [POPL'11] [POPL'14]. Designing new methods for the higher-order 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 Higher-Order Constrained Horn Clauses: A New Approach to Verifying Higher-Order Programs.
• UK Research Institute on Verified, Trustworthy Software Systems. A PhD studentship on Higher-Order 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 Curry-Howard correspondence.
• COMS20007: Programming Languages and Computation. An introduction to programming language theory and the theory of computation.