Abstract Operational Methods for Call-by-Push-Value
Goncharov S, Tsampas S, Urbat H (2025)
Publication Language: English
Publication Type: Journal article
Publication year: 2025
Journal
Book Volume: 9
Pages Range: 1013-1039
Article Number: 35
Journal Issue: POPL
DOI: 10.1145/3704871
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.
Authors with CRIS profile
Stylianos Tsampas
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Henning Urbat
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Involved external institutions
United Kingdom (GB)How to cite
APA:
Goncharov, S., Tsampas, S., & Urbat, H. (2025). Abstract Operational Methods for Call-by-Push-Value. Proceedings of the ACM on Programming Languages, 9(POPL), 1013-1039. https://doi.org/10.1145/3704871
MLA:
Goncharov, Sergey, Stylianos Tsampas, and Henning Urbat. "Abstract Operational Methods for Call-by-Push-Value." Proceedings of the ACM on Programming Languages 9.POPL (2025): 1013-1039.
BibTeX: Download