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}
}