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).
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, 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 (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 more accessible introduction to my POPL'23 work on a decidable fragment of higher-order Horn clauses and a deeper 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.
- 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 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.
- Toby Cathcart Burn, co-supervised with Luke Ong and funded by the University of Oxford.
- Eddie Jones, co-supervised with Luke Ong and funded by the VeTSS Research Institute.
- Charlie Walpole, funded by the University of Bristol.
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.