List Objects with Algebraic Structure. - Marcelo Fiore; Philip Saville (FSCD, 2017)

A type theory for cartesian closed bicategories (Extended Abstract). - Marcelo Fiore; Philip Saville (LICS, 2019)

A type theory for cartesian closed bicategories. - Marcelo Fiore; Philip Saville (CoRR, 2019)

Relative Full Completeness for Bicategorical Cartesian Closed Structure. - Marcelo Fiore; Philip Saville (FoSSaCS, 2020)

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure. - Marcelo Fiore; Philip Saville (LICS, 2020)

Cartesian closed bicategories: type theory and coherence. - Philip Saville (CoRR, 2020)

Coherence for bicategorical cartesian closed structure. - Marcelo Fiore; Philip Saville (Math. Struct. Comput. Sci., 2021)

Fully abstract models for effectful λ-calculi via category-theoretic logical relations. - Ohad Kammar; Shin-ya Katsumata; Philip Saville (Proc. ACM Program. Lang., 2022)

Strong pseudomonads and premonoidal bicategories. - Hugo Paquet; Philip Saville (CoRR, 2023)

Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd Bicategories. - Hugo Paquet; Philip Saville (ACT, 2023)

Clones, closed categories, and combinatory logic. - Philip Saville (FoSSaCS (2), 2024)

Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads. - Hugo Paquet; Philip Saville (LICS, 2024)

Logical relations for call-by-push-value models, via internal fibrations in a 2-category. - Pedro H. Azevedo de Amorim; Satoshi Kura 003; Philip Saville (CoRR, 2025)