Abstract Operational Methods for Call-by-Push-Value
Sergey Goncharov, Stelios Tsampas, Henning Urbat
TL;DR
This work develops a modular, categorical theory of program equivalence for call-by-push-value and its fine-grain variant FGCBV using Higher-Order Abstract GSOS. By modeling CBPV and FGCBV in presheaf categories with sorting into values and computations, it derives generic notions of applicative similarity and step-indexed logical relations whose soundness reduces to simple rule-based checks. The approach unifies operational reasoning for complex higher-order languages, including binding and effects, and yields modular proofs of contextually relevant congruences. The framework promises scalable tooling for reasoning about compilation targets and effectful languages, with future directions toward richer effects and rule formats.
Abstract
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-by-name 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.