A semantic model for verification of higher-order programs

We consider simply typed lambda-calculus with fixpoints as a
non-interpreted functional programming language: the result of the
execution of a program is its normal form that can be seen as a,
potentially infinite, tree of calls to built-in operations.  Properties
of such trees are properties of executions of programs and Monadic
second-order logic (MSOL) is well suited to express them.

For a given MSOL property we show how to construct a model recognizing it.
In other words, the value of a lambda-term in the model determines if the tree that is the result of the execution of the term satisfies the
property.  This construction allows to infer many results about
verification in this framework.