Abstract. We prove an n-exptime lower bound for the problem of deciding the winner in a reachability game on Higher Order Pushdown Automata (HPDA) of level n. This bound matches th...
Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that tθ and u have the same nor...
In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested ...
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H...
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 (progra...
Given a set P of natural numbers, we consider infinite games where the winning condition is a regular -language parametrized by P. In this context, an -word, representing a play, h...