4 citations · 8 across the 7 of their papers we have counts for
7 papers
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise…
Bicategories of algebras for relative pseudomonads
Nathanael Arkor, Philip Saville, Andrew Slattery
We introduce pseudoalgebras for relative pseudomonads and develop their theory. For each relative pseudomonad , we construct a free--forgetful relative pseudoadjunction that exh…
Clones, closed categories, and combinatory logic
Philip Saville
We give an exposition of the semantics of the simply-typed lambda-calculus, and its linear and ordered variants, using multi-ary structures. We define universal properties for mult…
Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd Bicategories
Hugo Paquet, Philip Saville
Premonoidal categories and Freyd categories provide an encompassing framework for the semantics of call-by-value programming languages. Premonoidal categories are a weakening of mo…
Effectful Semantics in Bicategories: Strong, Commutative, and Concurrent Pseudomonads
Hugo Paquet, Philip Saville
We develop the theory of strong and commutative monads in the 2-dimensional setting of bicategories. This provides a framework for the analysis of effects in many recent models whi…
Cartesian closed bicategories: type theory and coherence
Philip Saville
In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the r…
A type theory for cartesian closed bicategories
Marcelo Fiore, Philip Saville
We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that it…