steven.ramsay at bristol.ac.uk
Steven Ramsay
School of Computer Science
University of Bristol, UK

I am an Associate Professor in Programming Languages 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.

I am currently recruiting a Senior Research Assistant to work on Types for Incorrectness, a 3-year EPSRC-funded project to develop the theory and practice of a new foundation for typing that can both prove and refute type assignments. If you want to know what this type theory is like and what it is capable of, see our latest preprint (conditionally accepted to POPL’26): A Complementary Approach to Incorrectness Typing.

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

  • EPSRC. Research project on Types for Incorrectness (2026-2029).
  • Meta Research. Research project on Scalable Static Taint analysis for Core Erlang (2024).
  • EPSRC. Research project on Higher-Order Constrained Horn Clauses: A New Approach to Verifying Higher-Order Programs (2020-2023).
  • UK Research Institute on Verified, Trustworthy Software Systems. PhD studentship on Higher-Order Program Invariants (2020-2023).

PhD Students

  • Amos Holland, funded by the University of Bristol.
  • Chenghao Su, visiting from Nanjing University, China.
  • Celia Li, funded by the University of Bristol.
  • 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.