Reference. Logical relations for call-by-push-value models, via internal fibrations in a 2-category

Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville · LICS · 2025 · category-theory call-by-push-value logical-relations · Web · arXiv

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 the usual notion of sets-with-relations – provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.

Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics.

Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV.

Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata’s ⊤⊤-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.

Cite
Cite as @amorim_kura_saville_2025 (helia, typst) · \cite{amorim_kura_saville_2025} (LaTeX)
BibTeX
bibtex · 9 lines
@inproceedings{amorim_kura_saville_2025,
 title = {Logical relations for call-by-push-value models, via internal fibrations in a 2-category},
 author = {Amorim, Pedro H. Azevedo de and Kura, Satoshi and Saville, Philip},
 year = {2025},
 url = {https://arxiv.org/abs/2505.14482},
 booktitle = {Symposium on Logic in Computer Science (LICS 2025)},
 eprinttype = {arXiv},
 eprint = {2505.14482}
}
hayagriva YAML (typst)
yaml · 14 lines
amorim_kura_saville_2025:
  type: article
  title: Logical relations for call-by-push-value models, via internal fibrations in a 2-category
  author:
  - Amorim, Pedro H. Azevedo de
  - Kura, Satoshi
  - Saville, Philip
  date: 2025
  url: https://arxiv.org/abs/2505.14482
  serial-number:
    arxiv: '2505.14482'
  parent:
    type: proceedings
    title: Symposium on Logic in Computer Science (LICS 2025)
Download: amorim_kura_saville_2025.bib · amorim_kura_saville_2025.yml
Cited by (2)

A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version) amorim-2026-aarXiv · 2026
In this paper we present a framework for modelling reward-sensitive bisimulations, that is, bisimulations that account for quantitative differences such as accumulated rewards. To capture both qualitative and quantitative aspects uniformly, we consider two interacting notions of bisimulation: a graded variant that tracks bounded reward differences, and an ungraded one that abstracts from them. Our characterization of these notions is done in the fibrational and coalgebraic approach to (bi)simulation initiated by Hermida and Jacobs. To formally relate the graded and ungraded notions, we deploy categorical gluing, a standard technique in categorical logic. Furthermore, we show that this construction interacts well with standard coalgebra concepts, such as final coalgebras, and that it yields a unified characterization in terms of combined notions of bisimulations under mild assumptions. In order to demonstrate the versatility of our approach, we show how it encompasses various bisimulation notions for different kinds of systems, including relation-based bisimulations for automata with rewards and metric-based notions of bisimulations for labelled Markov processes.
arXiv

The Compositional Essence of Effectful Cost Analyses: Categorical Foundations and Fibered Logical Relations amorim_effcost2025
Web
Cites 78 works (10 here)
With notes (10)

Denotational Foundations for Expected Cost Analysis amorim_2025_oopslaOOPSLA · 2025

Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy.

In this work we introduce cert: a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip cert with an operational cost semantics and define two denotational semantics — a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics.

We formally relate both denotational semantics by stating and proving a novel effect simulation property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics.

Finally, we illustrate the expressivity of cert and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.

PDF · DOI · pldb

Semantic analysis of normalisation by evaluation for typed lambda calculus fiore-2022-semanticMSCS · 2022
This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper, the analysis is refined further by considering intensional Kripke relations (in the form of Artin–Wraith glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently typed functional programming language is synthesised.
DOI · arXiv

Fully abstract models for effectful λ-calculi via category-theoretic logical relations kammar-2022-fullyPOPL · 2022
We present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lifting, and ⊤⊤-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming.
PDF · DOI · pldb

Monoidal Grothendieck construction moeller_vasilakopoulou_2020TAC · 2020
We lift the standard equivalence between fibrations and indexed categories to an equivalence between monoidal fibrations and monoidal indexed categories, namely lax monoidal pseudofunctors to the 2-category of categories. Furthermore, we investigate the relation between this ‘global’ monoidal version where the total category is monoidal and the fibration strictly preserves the structure, and a ‘fibrewise’ one where the fibres are monoidal and the reindexing functors strongly preserve the structure, first hinted by Shulman. In particular, when the domain is cocartesian monoidal, we show how lax monoidal structures on a pseudofunctor to Cat bijectively correspond to lifts of the pseudofunctor to MonCat. Finally, we give some examples where this correspondence appears, spanning from the fundamental and family fibrations to network models and systems.
Web · arXiv

Framed bicategories and monoidal fibrations shulman_2008TAC · 2008

In some bicategories, the 1-cells are ‘morphisms’ between the 0-cells, such as functors between categories, but in others they are ‘objects’ over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the ‘morphisms between 0-cells’, such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change ‘nonalgebraically’, using categorical fibrations. The resulting ‘framed bicategories’ assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.

We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a ‘monoidal fibration’, meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Web

Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalueSemantic Structures in Computation · 2003
DOI

Categorical Logic and Type Theory jacobs-19991999

This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.

Notes on sconing and relators mitchell_scedrov_1993CSL · 1993
DOI

Two-dimensional monad theory blackwell_kelly_power_1989JPAA · 1989
Web

A general coherence result power_1989JPAA · 1989
External (68)
amorim_kura_saville_2025 reference entries/refs/amorim_kura_saville_2025/amorim_kura_saville_2025.hel