A denotational account of logical relations for call-by-push-value

Logical relations are a key tool in the semanticist's armoury. They play a central role in proofs of adequacy, in chararacterising definability, and in comparing different implementations of the same effect. From a denotational perspective, logical relations are elegantly captured by "fibrations for logical relations". These are fibrations---categorical axiomatisations of the structure of predicates / relations---which strictly preserve the interpretation of terms. This theory is well-developed for models of the simply-typed lambda calculus and monadic-style CBV languages with effects, but it is not obvious how to extend it to the more subtle setting of Levy's call-by-push-value (CBPV).

In this talk I will outline the existing theory, then show how taking a 2-categorical perspective leads naturally to a mathematically-justified definition of fibration---and hence logical relations---for CBPV. Because we use the general theory of fibrations in a 2-category, we also get a rich mathematical theory paralleling existing results for models of CBV. Along the way I will point out the commonalities between our approach for CBPV and the existing theory for CBV, and suggest that this is part of a more general pattern.

No prior knowledge of 2-categories or fibrations will be assumed.