I am a postdoc working with Liron Cohen at BGU. Before this, I was a postdoc at Birmingham with Vincent Rahli. I did my PhD in Computer Science at Oxford, supervised by Samson Abramsky. Prior to this, I completed as MS in Logic, Computation and Methodology across the Pond at CMU. My first degree was an MSci in Physics and Philosophy from Bristol.
I was born in Hexham, Northumberland, and grew up in Lichfield, Staffordshire. I am married to Julia. I play cricket, korfball and piano. I am in perpetual search for the next sticky bun.
s.l.speight at bham.ac.uk
News
Some papers to appear in CSL 2027!
Research
Keywords: Category theory, Type theory, Logic, Realizability
I am interested in the computational content of mathematics and logic, and the mathematical structure of logical and computational processes.
Papers
Proof-Relevant Realizability Models of Intensional Type Theory
To appear in CSL 2027
Sheaf Realizability for Dependent Type Theory
To appear in CSL 2027
Impredicativity in Linear Dependent Type Theory
With Niels van der Weide, to appear in CSL 2027
arXiv version
TPTL-DIST: A Calculus for Verifying Real-Time Distributed Systems
With Javier Enriquez Mendoza and Vincent Rahli, FORTE 2026
https://doi.org/10.1007/978-3-032-28187-6_12
Combinatory Completeness in Structured Multicategories
With Ivan Kuzmin, Chad Nester and Ülo Reimaa, RAMICS 2026
https://doi.org/10.1007/978-3-032-22469-9_16,
arXiv version
Groupoidal Realizability for Intensional Type Theory
MSCS: Advances in Homotopy Type Theory, 2024
https://doi.org/10.1017/S0960129524000343,
arXiv version
Impredicative Encodings of (Higher) Inductive Types
With Steve Awodey and Jonas Frey, LICS 2018
https://doi.org/10.1145/3209108.3209130,
arXiv version
Talks
Impredicativity in Linear Dependent Type Theory
PSSL 112, Nottingham, March 2026
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 SMLS, 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, University of 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 lecturer:
Lambda Calculus and Combinatory Algebra, Midlands Graduate School in Foundations of Computing Science (MGS), Nottingham, April 2026
The Nature of Mathematical Reasoning, CMU, Summer 2016 and Spring 2017
As tutor/TA/grader:
Mathematical and Logical Foundations of Computer Science, Birmingham, 2023
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
MGS
Lecture notesStuff
...