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, graduated 2024, now a Lecturer at 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 Curry-Howard correspondence.
- COMS20007: Programming Languages and Computation. An introduction to programming language theory and the theory of computation.