一句话：基于预层范畴与高阶抽象 GSOS，为 CBPV 和细粒度 CBV 建立模块化的程序等价推理方法。
Levy 的 call-by-push-value（CBPV）统一函数式与命令式编程，支持计算效应并涵盖 call-by-value 与 call-by-name；细粒度 call-by-value（FGCBV）是其轻量按值子语言。本文关注二者程序等价推理难以模块化扩展的问题。作者以排序集合的预层范畴作为建模 CBPV/FGCBV 的语义宇宙，在该框架内发展自然、余代数式的程序等价概念，如 applicative similarity 与逻辑关系。进一步将 FGCBV 和 CBPV 形式化到高阶抽象 GSOS（HOAS GSOS）中，利用已有理论把关键的合同性（congruence）性质归约为简单语法条件，并论证语言修改只需极小证明开销。结果为效应语言的等价推理提供可组合、可扩展的抽象操作语义方法。
Levy’s call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-byname evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.
@article{paperbot3225,
title = {Abstract Operational Methods for Call-by-Push-Value},
author = {Sergey Goncharov and Stelios Tsampas and Henning Urbat},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704871}
}