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 project: Design and Verification of Time-Critical Byzantine Fault-Tolerant Systems.

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

...

**Keywords**: type theory, category theory, realizability, distributed systems

**Computation**: I study the scope and limits of computation. Often, "computation" is taken to mean those actions that could be carried out by a machine, though it is interesting to note that original conception of "computer" was a human being following fixed rules.

**Language and logic**: For a given domain, can we capture and reason about it in a natural and convenient way?

**Structure**: How are things put together? What sort of inference does a particular structure support?

These interests manifest in the study of type theory and category theory. Category theory is the mathematics of structure (sometimes called the mathematics of mathematicsâ€”well, mathematics is all about structure, right?); it studies classes of objects and transformations between them. Type theories are formal languages, like logics, but where proofs (as in mathematics) and programs (as in computing) live as first-class citizens. Proofs and programs are actually the same kind of thing in type theory; this is part of the "Curry-Howard correspondence". Type theories are implemented in so-called "proof assistants" (such as *Agda*), which aid mathematicians in writing proofs (whilst simultaneously acting as programming languages).

Categorical models can be used to prove things about type theories (such as consistency results). Conversely, type theories provide "internal languages" for reasoning about/inside structured categories. The basic objects of a type theory may natively behave like objects that are otherwise complicated to construct; we say that type theory lets us reason *synthetically* about such objects.

The flavour of categorical model that much of my work to date has focused on is realizability models. Realizability reveals computational content of mathematical theories, and provides models of dependent and impredicative type theories. For my PhD, I developed higher-dimensional realizability models of intensional type theory based on groupoids, wherein realizers themselves carry higher-dimensional structure.

**Groupoidal realizability for intensional type theory**

Accepted for publication at *Mathematical Structures in Computer Science* special issue *Advances in Homotopy Type Theory*.
Preprint: arXiv:2405.19095

**Impredicative encodings of (higher) inductive types**

With Steve Awodey and Jonas Frey.

LICS 2018. doi:10.1145/3209108.3209130

**Higher-Dimensional Realizability for Intensional Type Theory**

PhD thesis, University of Oxford, supervised by Samson Abramsky.

**Impredicative encodings of inductive types in homotopy type theory**

Master's thesis, Carnegie Mellon University, supervised by Steve Awodey and Jonas Frey.

Available here.

**Proof-relevant partial equivalence relations**

6th SMLS, Oxford, slides

**Partial combinatory algebras for intensional type theory**

ACT 2024, Oxford

TYPES 2024, Copenhagen

**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**

Invited talk at *Practical and Foundational Aspects of Type Theory*, University of Kent, June 2018

**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

...