I am a Research Fellow in the School of Computer Science at the University of Birmingham, and part of the Theory of Computation research group. I work with Vincent Rahli on the Design and Verification of Time-Critical Byzantine Fault-Tolerant Systems project.
I did my DPhil (PhD) in Computer Science at the University of Oxford, supervised by Samson Abramsky. Before this, I spent a couple of years across the pond completing an MS in Logic, Computation and Methodology at Carnegie Mellon University, Pittsburgh. My first degree was an MSci in Physics and Philosophy from the University of Bristol.
I was born in Hexham, Northumberland, and grew up in Lichfield, Staffordshire. I am married to Julia. I like circket (especially a crisp cover drive), music (especially playing the piano) and food (especially cheese).
s.l.speight at bham.ac.uk
Office 242
School of Computer Science
University of Birmingham
B15 2TT
UK
News
...
Research
Keywords: Category theory, Type theory, Logic, Realizability
Papers
Combinatory Completeness in Structured Multicategories With Ivan Kuzmin, Chad Nester and Ülo Reimaa. RAMICS 2026.
Groupoidal realizability for intensional type theory MSCS: Advances in Homotopy Type Theory, 2024. doi:10.1017/S0960129524000343
Impredicative encodings of (higher) inductive types. With Steve Awodey and Jonas Frey. LICS 2018. doi:10.1145/3209108.3209130
Talks
Combinatory Completeness in Structured Multicategories
Category Theory Working Group, Manchester, December 2025
Computing up to Isomorphism: Proof-Relevant PERs
Réalisabilité, CIRM, April 2025, slides
Computation up to Isomorphism: Higher-Dimensional Realizability
Dame Kathleen Ollerenshaw annual workshop: Categorical Logic and Higher Categories, Manchester, December 2024, slides
Proof-Relevant Partial Equivalence Relations
6th Southern and Midlands Logic Seminar, Oxford, June 2024, slides
Partial Combinatory Algebras for Intensional Type Theory
ACT 2024, Oxford, slides, recording
TYPES 2024, Copenhagen, extended abstract
Groupoidal Realizability for Intensional Type Theory
Category Theory Seminar, Manchester, Nov 2023
Groupoidal Realizability over Cubical Lambda-Calculus
HoTT 2023, CMU, slides
Higher-Dimensional Realizability for Intensional Type Theory
CMU HoTT Seminar, November 2022
Groupoidal Realizability: Formalizing the Topological BHK Interpretation of Intensional Type Theory
LoVe Seminar, University of Paris 13, May 2022
Logic and Higher Structures, CIRM, February 2022
Impredicative Encodings of (Higher) Inductive Types
LICS 2018, Oxford
Encoding Inductive Types in Impredicative Intensional Dependent Type Theory
Practical and Foundational Aspects of Type Theory, Kent, June 2018
Theses
Higher-Dimensional Realizability for Intensional Type Theory. PhD thesis, University of Oxford (supervised by Samson Abramsky), 2023. Available here
Impredicative encodings of inductive types in homotopy type theory Master's thesis, Carnegie Mellon University (supervised by Steve Awodey and Jonas Frey), 2017. Available here
Teaching
As instructor:
The Nature of Mathematical Reasoning, CMU, Summer 2016 and Spring 2017
As tutor/TA/grader:
Models of Computation, Oxford (Wycliffe Hall), Michaelmas 2021
Categories, Proofs and Processes, Oxford (Computer Science), Michaelmas 2019 and 2020
Formal Logic, CMU, Fall 2016
Ethical Theory, CMU, Spring 2016
Engineering Ethics, CMU, Fall 2015
Stuff
...