Our objective is to verify behavioural properties of programs, as for example "an open stream is eventually closed", or "a login function is called infinitely often". We use lambda Y-calculus, the simply typed lambda-calculus with the fixpoint combinator, as an intermediate language. The approach we pursue consists of two steps: translate a program into a term of lambda Y-calculus, and then analyse the Bohm tree of the resulting term. Thanks to the result of Ong it is decidable if the Bohm tree of a given term satisfies a given property expressed in monadic second-order logic; this is a classical logic for tree properties that is capable to express many interesting properties of computations. We solve the verification problem by a mix of automata and semantic techniques, in particular we construct appropriate models of lambda Y calculus.

The talk will start with the introduction to the verification problem for higher-order programs. Most type systems for programming languages concentrate on, some, safety properties of programs. We will present monadic second-order logic (MSOL) on binary trees, and give indications why verification of MSOL properties is more complex than just for safety properties. Next, we will adapt the notion of recognizability, the classical notion from language theory, to our setting. We will state our main result saying that for every MSOL property there is a finitary model of the lambda Y-calculus recognizing this property. Finally, we will discuss some corollaries of this theorem concerning verification of programs as well as program transformation, and program synthesis.

This is joint work with Sylvain Salvati.