Parks Road, Oxford OX1 3QD
My primary research interests are type theory and category theory. My work usually falls under the umbrella "logic in computer science", but I am interested in applications of the above in general.
For my DPhil I am developing groupoidal versions of realizability models and game semantics for intensional type theory.
I also try to maintain an interest in philosophy of mathematics and quantum (information) 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, gave impredicative encodings of inductive types with their full universal properties (eta-rules, dependent eliminators) in intensional dependent type theory, making essential use of identity types.
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.
Details about Impredicative Encodings of (Higher) Inductive Types | BibTeX data for Impredicative Encodings of (Higher) Inductive Types | DOI (10.1145/3209108.3209130) | Link to Impredicative Encodings of (Higher) Inductive Types