Verification on higher-order recursive schemes

We propose a new approach to analysing higher-order recursive
schemes. Higher-order recursive schemes were introduced by Damm in the
80-ties as a respelling of simply-typed lambda calculus with fixpoints
(lambda-Y). In this century the interest in higher-order schemes has
been renewed by the discovery by Knapik, Niwinski and Urzyczyn of the
equivalence between higher-order pushdown automata of order n and
schemes of order n satisfying a syntactic constraint called
safety. Later Ong has proved that trees generated by recursive schemes
without safety restriction have decidable monadic second-order theory.

We will present two new approaches to annalysing recursive
schemes. The first one uses stadandard models of lambda-Y. The second
uses evaluation  model called Krivine machine.  Both methods are quite
standard in the lambda-calculus community, but have not yet been
applied to verification problems. We will show that they are extremely
well adapted to the task.