4 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…
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…
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…