Game semantics and higher-order pushdown automata with links

Knapik et al have recently shown that, as generators of trees,
higher-order pushdown automata (HOPDA) are equivalent to higher-order
recursion schemes that satisfy a syntactic constraint called safety.
We study a variant class of HOPDAs in which items in the stack
(level-n, say) may have links (or pointers) to m-stacks (m <= n) lower
down.  When such an item is on top_1 of the n-stack, the effect of a
special "collapse" instruction is pop the appropriate top stacks, so
as to cause the m-stack that is pointed to to surface to the top. We
show that such machines may be regarded as an automata-theoretic
characterization of higher-order recursion schemes (whether safe or
not) in that they compute precisely the innocent game semantics of
these schemes.