To model-check a higher-order functional program with recursion, one can abstract it as a lambda Y-term normalizing to a tree over a signature of actions, which approximates the set of behaviours of this program. Running an alternating parity automaton over this tree is then a way to ensure that it respects a given MSO specification.

A connection between higher-order model-checking and linear logic appears naturally when one considers the linear typing of lambda-terms. Interpreted in the relational model of linear logic, the duals of these types correspond precisely to the set of alternating automata (without parity condition), leading to a semantic model-checking approach: lambda-terms generating trees and alternating tree automata are given dual semantics in the relational model, so that their interaction computes the set of states from which an automaton accepts the tree computed by a term. The model-checking problem may then be solved by checking that the initial state of the automaton belongs to the result.

In this talk, we explain how this theorem can be generalized to lambda-terms with recursion, and to alternating automata with a parity condition. This requires us to consider an infinitary variant of the relational semantics of linear logic, and to define a coloured exponential modality over it. We finally devise a fixed point operator verifying directly at the level of denotations the parity condition of alternating parity tree automata, and obtain the desired generalized semantic model-checking theorem.

We finally recast our approach in a finitary model of linear logic, provided by its Scott semantics, and explain how it leads to a decidability proof of the higher-order model-checking problem.

(joint work with Paul-André Melliès)