Philip Saville

philip.saville [at] cl.cam.ac.uk / philip.saville [at] ed.ac.uk

As of June 2019 I have started a post-doc with Ohad Kammar at the University of Edinburgh (my new webpage is here). I am also finishing my thesis proving a coherence theorem for cartesian closed bicategories using a normalisation-by-evaluation style argument.

I am a PhD student with Marcelo Fiore in the Programming, Logic and Semantics group of the Computer Lab at the University of Cambridge. My work uses category theory to study mathematical structures that arise in theoretical computer science and mathematics; I am particularly interested in the perspective of universal algebra and the related abstract syntax approach to studying type theories.

Publications

• A type theory for cartesian closed bicategories, with Marcelo Fiore. Accepted to LICS 2019 (pre-print available here).

• List objects with algebraic structure (pdf, talk slides), with Marcelo Fiore. FSCD 2017.

Talks

• Skew monoidal structures in categories of algebras, with Marcelo Fiore. At Category Theory 2018, University of Azores, Ponta Delgada, Portugal. Slides available here.

Teaching and other activities

I have supervised Discrete Maths, Semantics of Programming Languages, Logic and Proof, Denotational Semantics and Types. I was also co-convenor of the PLS group's informal seminar series, Logic & Semantics for Dummies.