Abstract Operational Methods for Call-by-Push-Value

Explore a 25-minute conference talk from POPL 2025 where researchers Sergey Goncharov, Stelios Tsampas, and Henning Urbat present their work on developing modular reasoning methods for program equivalence in call-by-push-value and fine-grain call-by-value programming paradigms. Learn how the team leverages presheaf categories of sorted sets as suitable modeling universes and applies coalgebraic notions like applicative similarity and logical relations to establish program equivalence. Discover how they formalize these languages within the higher-order abstract GSOS framework, reducing key congruence properties to simple syntactic conditions while minimizing proof overhead when introducing language changes. The presentation covers categorical semantics and demonstrates how Levy's call-by-push-value paradigm effectively combines functional and imperative programming elements while supporting computational effects.