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.