Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909648190177280 |
|---|---|
| author | de Amorim, Pedro H. Azevedo Kura, Satoshi Saville, Philip |
| author_facet | de Amorim, Pedro H. Azevedo Kura, Satoshi Saville, Philip |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_14482 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Logical relations for call-by-push-value models, via internal fibrations in a 2-category de Amorim, Pedro H. Azevedo Kura, Satoshi Saville, Philip Logic in Computer Science Category Theory 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. |
| title | Logical relations for call-by-push-value models, via internal fibrations in a 2-category |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2505.14482 |