4 citations · 5 across the 5 of their papers we have counts for
5 papers · 1 filter
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…
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…
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…