Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees

ABSTRACT. We introduce type-checking games, which are omega-regular games over Boehm trees, determined by a type of the Kobayashi-Ong intersection type system. These games are a higher-type extension of parity games over trees, determined by an alternating parity tree automaton. However, in contrast to these games over trees, the "game boards" of our type-checking games are composable, using the composition of Boehm trees. Moreover the winner of a composite game is completely determined by the respective winners of the component games.

To our knowledge, type-checking games give the first compositional analysis of higher-order model checking, or the model checking of trees generated by recursion schemes. We study a higher-type analogue of higher order model checking, namely, the problem to decide the winner of a type-checking game over the Boehm tree generated by a lambda-Y-term. We introduce a new type system and use it to prove that the problem is decidable.

On the semantic side, we develop a novel arena game model for type-checking games, which is a cartesian closed category equipped with parametric monad and comonad that themselves form a parametrised adjunction.