Abstract Operational Methods for Call-by-Push-Value

TL;DR

This paper introduces modular methods for reasoning about program equivalence in call-by-push-value and fine-grain call-by-value languages, using presheaf categories and coalgebraic notions to simplify proofs.

Contribution

It formalizes call-by-push-value and fine-grain call-by-value within the higher-order abstract GSOS framework, enabling minimal overhead in proving language properties.

Findings

Presheaf categories model call-by-(push)-value languages effectively.

Coalgebraic notions like applicative similarity are applicable for program equivalence.

The approach simplifies proving congruence properties in these languages.

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.