Philip Saville
(firstname).(lastname)@ed.ac.uk
As of February 2021 I have moved to Oxford: my new website is here.
I am currently a post-doc working with Ohad Kammar
as part of the grant Effectful theories of programming languages:
models, abstractions, validation.
Before that I was a PhD student of Marcelo Fiore
at the University of Cambridge.
Research interests
I am interested in category theory and its applications to theoretical computer science.
Particularly:
- Categorical semantics of programming languages.
- Categorical universal algebra.
- Higher-dimensional categories: their internal languages, proofs of coherence,
and applications to rewriting theory and proof theory.
Publications
Thesis
Cartesian closed bicategories:type theory and coherence, supervised
by Marcelo Fiore. Examined by Steve Awodey (external) and Martin Hyland (internal),
24th March 2020.
- Version for on-screen viewing here.
- Version for print here.
Selected talks
- Normalisation-by-evaluation for coherence of cartesian closed bicategories
(slides),
Oxford Advanced Seminar on Informatic Structures (OASIS), Department of
Computer Science, University of Oxford, March 2020
- A type theory for cartesian closed bicategories
(slides - updated to correct a small mistake),
with M. Fiore. Category Theory 2019, July 2019, Edinburgh.
- Skew monoidal structures on categories of algebras
(slides), with M. Fiore. Category
Theory 2018, July 2018, Azores, Portugal.