Philip Saville

I am currently a post-doc with Sam Staton. Previously I was a post-doc at the University of Edinburgh working with Ohad Kammar as part of the grant Effectful theories of programming languages: models, abstractions, validation. Before that I was a PhD student under Marcelo Fiore at the University of Cambridge.

Research interests

I am interested in category theory and its applications to theoretical computer science. Particularly:

1. Categorical semantics of programming languages.
2. Categorical universal algebra.
3. Higher-dimensional categories: their internal languages, proofs of coherence, and applications to rewriting theory and proof theory.

Publications

• Fully abstract models for effectful λ-calculi (preprint), with O. Kammar and S.-y. Katsumata. Principles of Programming Languages (POPL) 2022.
  DOI: 10.1145/3498705.
• Coherence for bicategorical cartesian closed structure (preprint), with M. Fiore. Festschrift in honour of John Power, Mathematical Structures in Computer Science (MSCS) 2021.
  DOI: 10.1017/S0960129521000281.
• 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

• Full abstraction à la O’Hearn–Riecke (slides), with O. Kammar & S. Katsumata. Cambridge Logic and Semantics Seminar, Department of Computer Science and Technology, Nov. 2020.
• 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
• Synthesising a type theory for cartesian closed bicategories (slides), Partout Seminar, Paris, January 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.