Higher-order model checking is a generalization of finite-state model checking, obtained by replacing finite-state models with more expressive models called higher-order recursion schemes (HORS). From a programming language perspective, HORS may be viewed as a simply-typed functional program for generating an infinite tree, and higher-order model checking is concerned with checking properties of the tree generated by HORS. Higher-order model checking is an interesting and challenging topic from both theoretical and practical perspectives. On the theoretical side, it has rich theories, with connections to various topics of theoretical computer science, including λ-calculus, type theories (intersection types, in particular), game semantics, and formal languages/automata theory. On the practical side, it enables fully automated verification of higher-order programs.

The tutorial will start with a gentle introduction to higher-order model checking and its historical background, and cover both theories and applications of higher-order model checking, with an emphasis on applications to program verification.

The tutorial consists of 90 minutes, given twice at 8:30-10:00, and 16:00-17:30.