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


I am a senior lecturer in the Programming Languages Group in the Department 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 and then let me know which papers you are interested in.

Current Research

My research is on program analysis and automated reasoning, especially for applications in program verification. See here for a full list of my publications.

  • Tools for functional programming [POPL'21] [PLDI'22]. Designing tools based on automated reasoning to help programmers write bug-free code.
  • Fragments of higher-order logic [POPL'18] [LICS'21]. Identifying and exploiting fragments of higher-order logic that have good computational properties.
  • Automata over infinite alphabets [LICS'15] [JCSS'17]. Classifying foundational problems for register automata by their computational complexity.
  • Higher-order model checking [POPL'11] [POPL'14]. Designing new methods for the higher-order extension of software model checking.

Funded Projects
  • 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
  • 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.
Current Teaching

I run the following two courses at the University of Bristol:

  • COMS30040: Types and Lambda Calculus. An introduction to the pure, untyped lambda calculus, ML-style type systems and the Curry-Howard correspondence.
  • COMS20007: Programming Languages and Computation. An introduction to automata theory, programming language theory and the theory of computation.