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

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).


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.


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.