Operational Algorithmic Game Semantics for Call-by-Push-Value Calculus

Explore a 21-minute conference talk on operational algorithmic game semantics presented at GALOP'24 by Benedict Bunting and Andrzej Murawski. Delve into a simply-typed call-by-push-value calculus with state and its fully abstract trace model using a labelled transition system (LTS). Learn about optimisation techniques based on name recycling and discover how the LTS can be transformed into a deterministic visibly pushdown automaton for a specific fragment, leading to decidability of contextual equivalence and exponential-time solvability for terms in canonical form. Examine the identification of a fragment where these automata become finite-state machines. Understand how the trace model proves full abstraction for translations of call-by-name (IA) and call-by-value (RML) languages into the call-by-push-value language, encompassing various literature results for IA and RML. Gain insights into this operational approach as a simpler and more intuitive method for deriving such results, utilizing techniques rooted in operational semantics and resulting in automata that capture the language's underlying dynamics.