There are two kinds of higher-order extensions of model checking: HORS model checking
and HFL model checking. Whilst the former has been applied to automated verification of …

In this paper, we explain how the connection between higher-order model-checking and
linear logic recently exhibited by the authors leads to a new and conceptually enlightening …

We introduce type-checking games, which are ω-regular games over Böhm trees,
determined by a type of the Kobayashi-Ong intersection type system. These games are a …

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 …

This thesis studies problems of higher-order model-checking from a semantic and logical
perspective. Higher-order model-checking is concerned with the verification of properties …

This article studies the logical properties of a very general class of infinite ranked trees,
namely, those generated by higher-order recursion schemes. We consider, for both monadic …

We consider lambda-Y-calculus as a non-interpreted functional programming language: the
result of the execution of a program is its normal form that can be seen as the tree of calls to …

We propose an automated method for disproving fair termination of higher-order functional
programs, which is complementary to Murase et al.'s recent method for proving fair …

The lambda Y-calculus with priorities is a variant of the simply-typed lambda calculus
designed for higher-order model-checking. The higher-order model-checking problem asks …

We consider nondeterministic higher-order recursion schemes as recognizers of languages
of finite words or finite trees. We propose a type system that allows to solve the simultaneous …