Higher-order model-checking, categorical semantics, and linear logic

The verification of higher-order recursive programs is a challenging issue, for which model-checking techniques have been considered. Programs are abstracted using higher-order recursion schemes (HORS); and a recursion scheme G can be understood as a simply-typed λ-term with fixpoint operators Y, over a set Σ = a, b, c... of free variables of order at most one. In the spirit of a Church encoding, the set Σ can be seen as a ranked alphabet, over which the normalization of G computes a potentially infinite value tree 〈G〉, typically approximating the set of behaviors of a functional program. The higher-order model-checking problem then consists in checking whether a monadic second-order logic (MSO) formula φ holds at the root of 〈G〉. A convenient approach is to translate φ into an equivalent alternating parity tree automaton (APT) Aφ, a kind of non-deterministic top-down tree automaton enriched with alternation and coloring. A transition over a binary symbol a is typically of the form δ(q0, a) = (2, q2) ∨ ((1, q1) ∧ (1, q2) ∧ (2, q0)) (1