Philip Saville headshot

Philip Saville

Department of Computer Science, University of Oxford


Departmental webpage:; OrcID: 0000-0002-8320-0280

I am currently a post-doc with Sam Staton at the University of Oxford. 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.




Cartesian closed bicategories: type theory and coherence, supervised by Marcelo Fiore. Examined by Steve Awodey (external) and Martin Hyland (internal), 24th March 2020.

Selected talks


I am generally interested in supervising 3rd / 4th year projects on topics including category theory, 2-dimensional semantics, denotational semantics, and universal algebra with applications to programming language theory.