Verification of Higher-Order Computation: A Game-Semantic Approach

Abstract. We survey recent developments in an approach to the verification of higher-order computation based on game semantics. Higherorder recursion schemes are in essence (programs of) the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. They are a highly expressive definitional device for infinite structures such as word languages and infinite ranked trees. As applications of a representation theory of innocent strategies based on traversals, we present a recent advance in the model checking of trees generated by recursion schemes, and the first machine characterization of recursion schemes (by a new variant class of higher-order pushdown automata called collapsible pushdown automata). We conclude with some speculative remarks about reachability checking of functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and verification. Game semantics has emerged as a powerful par...

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: C.-H. Luke Ong
• Keywords: Algorithmic Game Semantics, ESOP 2008, Game Semantics, Programming Languages, Recursion Schemes