We survey recent developments in a systematic approach to the verification of higher-order computation based on two models: (the respective higher-order hierarchies of) recursion schemes and pushdown automata. Higher-order recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. Higher-order pushdown automata are a generalisation of pushdown automata to higher-order stacks, which are iterations of stack of stacks. They are highly expressive definitional devices for word languages and such infinite structures as trees and graphs. We study the expressive power of the two models and the algorithmic properties of the infinite structures generated by them. As an algorithmic application of game semantics, we present recent results in the model checking of infinite trees generated by recursion schemes, and a machine characterisation of recursion schemes by a new variant of higher-order pushdown automata called collapsible pushdown automata. We survey recent advances in the solution of parity games over the configuration graphs of collapsible pushdown automata. We conclude with some remarks on an application to the verification of higher-order functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and verification.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com