We consider a simply-typed call-by-push-value calculus with state, and provide a fully abstract trace model via a labelled transition system (LTS) in the spirit of operational game semantics. By examining the shape of configurations and performing a series of natural optimisation steps based on name recycling, we identify a fragment for which the LTS can be recast as a deterministic visibly pushdown automaton. This implies decidability of contextual equivalence for the fragment identified and solvability in exponential time for terms in canonical form. We also identify a fragment for which these automata are finite-state machines.
Further, we use the trace model to prove that translations of prototypical call-by-name (IA) and call-by-value (RML) languages into our call-by-push-value language are fully abstract. This allows our decidability results to be seen as subsuming several results from the literature for IA and RML. We regard our operational approach as a simpler and more intuitive way of deriving such results. The techniques we rely on draw upon simple intuitions from operational semantics and the resultant automata retain operational style, capturing the dynamics of the underlying language.
This is joint work with Benedict Bunting (University of Oxford).