Philip Saville

I am an assistant professor in computer science at the University of Sussex. Until September 2024 I was 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 a theoretical computer scientist interested in category theory and its applications to the foundations of programming language theory. My work has two common themes: (1) using ideas from logic to study the structure of programming languages; (2) using ideas from algebra to study the relationships between denotational models, and hence better understand common techniques in semantics. In particular, my interests include:

1. Categorical semantics of programming languages, especially semantic models that contain extra information over traditional models (e.g. 2-dimensional models) and the algebraic foundations of techniques such as logical relations.
2. Categorical universal algebra, including multi-ary semantic models such as clones and multicategories.
3. Higher-dimensional categories: their internal languages, proofs of coherence, and applications to rewriting theory and proof theory.

Publications

• Logical relations for call-by-push-value models, via internal fibrations in a 2-category (ArXiv version, slides), with P. H. Azevedo de Amorim and S. Kura. Logic in Computer Science (LICS) 2025.
• Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads (authors' final version, ArXiv version), with H. Paquet. Logic in Computer Science (LICS) 2024.
  DOI: 10.1145/3661814.3662130.
• Clones, closed categories, and combinatory logic (submitted version, version with more proofs (on ArXiv), slides), Foundations of Software Science and Computation Structures (FoSSaCS) 2024.
  DOI: 10.1007/978-3-031-57231-9_8.
• Effectful semantics in 2-dimensional categories: premonoidal and Freyd bicategories (slides, paper, version with more proofs), with H. Paquet. Applied Category Theory (ACT) 2023.
  DOI: 10.4204/EPTCS.397.12.
• Fully abstract models for effectful λ-calculi (preprint, slides), 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, slides), with M. Fiore. Foundations of Software Science and Computation Structures (FoSSaCS) 2020.
  DOI: 10.1007/978-3-030-45231-5_15
• 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

• Logical relations for CB(P)V. Sussex FoSS Seminar, Feb. 2025. Slides here.
• Multi-ary models of programming languages. Bristol PL Seminar, Feb. 2024.
• Refined syntax and semantics, via taking contexts seriously. Directions and Perspectives in the Lambda Calculus. Bologna, Jan. 2024.
• Premonoidal bicategories (slides, with a few typos). Quantum Lunch, Oxford, June 2023.
• Diffeological spaces as a model for differentiable programs: a tutorial (slides). Global Diffeology Seminar, Sept. 2022.
• Logical relations, fibrations and definability (slides), with O. Kammar & S. Katsumata. TallCat Seminar, Apr. 2022.
• Constructing fully abstract models of effectful λ-calculi (slides), with O. Kammar & S. Katsumata. Birmingham Logic Seminar, Dec. 2021.
• Full abstraction a la O’Hearn–Riecke (slides, video), 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.

Teaching

I am generally interested in supervising projects on topics around theoretical computer science -- feel free to email me if you are interested!

• In 2024-5 I taught the Programming Concepts course.
• In 2022 I co-supervised (with Sam Staton) Lili Janzer's MSc thesis, titled Category-theoretic syntactic models of programming languages. A copy is available here.
• In 2021-22 I was TA for the Principles of Programming Languages course.
• As a PhD student I supervised (small-group teaching) the following courses: Discrete Maths, Logic and Proof, Types, Denotational Semantics.