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

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure (preprint, slides) with M. Fiore. Logic in Computer Science (LICS) 2020.
DOI: 10.1145/3373718.3394769.
Relative full completeness for bicategorical cartesian closed structure (preprint), with M. Fiore. Foundations of Software Science and Computation Structures (FoSSaCS) 2020.
A type theory for cartesian closed bicategories (preprint, slides - updated to correct a small mistake, erratum), with M. Fiore. Logic in Computer Science (LICS) 2019.
DOI: 10.1109/LICS.2019.8785708.
List objects with algebraic structure (preprint, slides), with M. Fiore. Formal Structures for Computation and Deduction (FSCD), Sept. 2017, Oxford.
DOI: 10.4230/LIPIcs.FSCD.2017.16.

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.