  In this article, we develop a new and somewhat unexpected connection between
higher-order model-checking and linear logic. Our starting point is the
observation that once embedded in the relational semantics of linear logic, the
Church encoding of any higher-order recursion scheme (HORS) comes together with
a dual Church encoding of an alternating tree automata (ATA) of the same
signature. Moreover, the interaction between the relational interpretations of
the HORS and of the ATA identifies the set of accepting states of the tree
automaton against the infinite tree generated by the recursion scheme. We show
how to extend this result to alternating parity automata (APT) by introducing a
parametric version of the exponential modality of linear logic, capturing the
formal properties of colors (or priorities) in higher-order model-checking. We
show in particular how to reunderstand in this way the type-theoretic approach
to higher-order model-checking developed by Kobayashi and Ong. We briefly
explain in the end of the paper how his analysis driven by linear logic results
in a new and purely semantic proof of decidability of the formulas of the
monadic second-order logic for higher-order recursion schemes.
