一句话：用 2-范畴内部纤维化为 CBPV 建立逻辑关系语义框架，并给出 ⊤⊤-lifting、效应模拟与相对完全性等实例。
本文在 Hermida、Jacobs、Katsumata 等人的纤维化风格下，为 call-by-push-value（CBPV）建立逻辑关系的指称语义。CBPV 模型同时含伴随与富集结构，直接定义合适的纤维化并不清楚；作者借助 2-范畴理论，将 CBPV 纤维化定义为合适 2-范畴内部的、严格保持 CBPV 语义的纤维化。随后给出与经典情形平行的理论，包括 codomain 与 subobject 纤维化的版本，并证明可通过拉回从旧模型构造新模型，从而构造新的逻辑关系式 CBPV 模型。最后用 Katsumata 的 ⊤⊤-lifting 的推广、效应模拟结果以及无非和类型 CBPV 的相对完全性结果展示框架的效用。
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.
DOI 原文 ·
@inproceedings{paperbot8654,
title = {Logical relations for call-by-push-value models, via internal fibrations in a 2-category},
author = {Pedro H. Azevedo de Amorim and Satoshi Kura and Philip Saville},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00061}
}