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

TL;DR

This paper develops a fibrational framework within 2-category theory to construct logical relations models for call-by-push-value, enabling analysis of effects and properties like effect simulation and full completeness.

Contribution

It introduces a novel 2-categorical notion of CBPV fibrations, extending fibrational models to handle CBPV's complex semantics with effects and adjunctions.

Findings

Constructed new logical relations models for CBPV

Generalized Katsumata's $ op op$-lifting to CBPV

Proved effect simulation and full completeness results

Abstract

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 $\top\top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.