My primary interest is type theory and its semantics. A bit more generally, I am interested in logic and category theory.
I am a DPhil (PhD) Candidate, supervised by Professor Samson Abramsky, in the Department of Computer Science, University of Oxford. I am a member of Oriel College and I am funded by an EPSRC Doctoral Training Partnership Studentship.
Before coming to Oxford, I completed a MS in Logic, Computation and Methodology at Carnegie Mellon University, Pittsburgh. My thesis, supervised by Professor Steve Awodey and Doctor Jonas Frey, uses ideas from homotopy type theory to give (refined system F) impredicative encodings of inductive types with dependent elimination (induction principles, their full universal properties).
Prior to this, I obtained an MSci in Physics and Philosophy with First Class Honours from the University of Bristol.
Impredicative Encodings of (Higher) Inductive Types
Steve Awodey‚ Jonas Frey and Sam Speight
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. Pages 76–85. New York‚ NY‚ USA. 2018. ACM.