Pushdown Automata and Game Semantics

Our goal is to study the algorithmic properties of, and develop verification techniques for, classes of infinite-state sequential systems (incuding automata and game models) that are abstract and accurate models of computation for appropriate fragments of Higher-Order Procedural Languages, or HOPL, for short. A language that exemplifies the richness of HOPL is Idealized Algol, a compact language that elegantly combines state-based procedural programming with higher-order functional features, mediated by a simple type theory; better known examples of HOPL are ML and C. The simplest and prototypical such models of computation are the deterministic pushdown automata (DPDA). We plan to construct an "efficient" implementation of an equivalence-checker for real-time DPDA, and use it as the engine of a tool for verifying observational equivalence and temporal properties of low-order fragments of (recursion-free) Idealized Algol. Our semantics-based approach has several advantages: we obtain a fullyautomatic verifier that is compositional (as our model checker applies directly to terms-in-context); further, thanks to the underpinning fully abstract game semantics, soundness and completeness are systematically guaranteed. The remainder of this proposal concerns the verification of recursively-defined HOPL programs, especially those at the low end of the type hierarchy. We shall examine old (e.g. higher-order recursion schemes) and seek new algorithmic representations of classes of recursive programs (e.g. higherorder pushdown trees augmented by lambda-binders or generalized Beohm trees) that accurately model the binding mechanisms of higher-order variables. We aim to develop algorithmic techniques for equivalence-checking and model-checking these models of computation. This project will be jointly investigated by C. P. Stirling (University of Edinbrugh) and C.-H. L. Ong (University of Oxford).