Finite state model checking has been widely studied and successfully applied to system verification. The main theme of this meeting, higher-order model checking, is a generalization of finite state model checking, obtained by replacing finite state models with more expressive models called recursion schemes. Higher-order model checking has found applications in analysis of object-oriented and concurrent programs with recursion and higher-order procedures.

Recursion schemes are a kind of simply-typed grammar for generating possibly infinite ranked trees. A recursion scheme is a finite system of equations, defining a finite set of higher-order functions by mutual recursion. The order of a recursion scheme is given by the highest type-theoretic order of the functions defined by it. From a programming language perspective, recursion schemes may be viewed as programs (i.e. closed, ground-type terms) of the simply-typed lambda calculus with recursion, constructed from a set of uninterpreted function symbols. Higher-order model checking is the model checking of trees generated by recursion schemes. The higher-order model checking problem asks, given a recursion scheme G and a correctness property φ, whether the tree generated by G satisfies φ.

The early work in the 1970s on (tree-generating) higher-order recursion schemes was mostly about questions of expressivity. The decision problem was first posed in the present form by Knapik et al. [5, 6]. They considered recursion schemes subject to a syntactic constraint called safety. Their main result is that, when restricted to trees generated by safe recursion schemes, the higher-order model checking problem with respect to monadic second- order (MSO) properties is decidable. However the general MSO higher-order model checking problem was left open. In [12], Ong proved that the modal mu-calculus model checking problem of trees generated by arbitrary order-n recursion schemes is n-EXPTIME complete. Since MSO logic and the modal mu-calculus are equi-expressive over trees, the MSO higher-order model checking problem is decidable.

The last fifteen years or so have seen a growth of interest in higher-order model checking from both the theory and practice communities. Since the MSO decidability result [12], which was proved using insights from game semantics [4], a variety of semantic and algorithmic techniques and models of computation have been employed to design higher-order model checking algorithms, notably, intersection types [7, 11], collapsible pushdown automata [3] and Krivine machines [15]. Algorithmic properties that refine and extend the decidability of MSO local model checking have also been introduced, such as logical reflection [1], effective selection [2] and transfer theorem [16]. One recent trend, initiated by Salvati and Walukiewicz, is the development of effective denotational semantics for an approach to higher-order model checking by evaluation [18, 17, 21].

Recursion schemes are a very expressive family of generators of trees: the trees that are generated at orders 0, 1 and 2 are respectively the regular trees, algebraic trees (i.e. those generated by context-free tree grammars) and hyperalgebraic trees. There have been advances in the understanding of the relationship between higher-order families of generators. Hague et al. [3] showed that order-n recursion schemes generate the same class of trees as order-n collapsible pushdown automata. More recently, Parys [13] proved the Safety Conjecture, thus confirming the intuition that the safety constraint restricts the expressive power of recursion schemes, or equivalently that order-n collapsibile pushdown automata are more expressive than order-n pushdown automata.

Recursion schemes are thus an appealing abstract model for model checking higher-order programs: not only are they highly expressive, the trees they generate also enjoy a rich and decidable logical theory. In [7, 8], Kobayashi introduced an approach to the verification of safety properties of functional programs by reduction to higher-order model checking. His verification method is sound, complete, and automatic for a range of verification problems such as reachability, flow analysis, and resource usage for simply-typed recursive functional programs generated from finite base types. Although the worst-case complexity of higher-order model checking is hyper-exponential, there have been remarkable advances in the design of model checking algorithms. The time complexity of state-of-the-art model checking algorithms, PREFACE [14] and HORSATZDD [19], are fixed-parameter polynomial in the size of the recursion schemes, and scale readily to many thousands of rules. In addition to the model checking of object-oriented [9] and concurrent programs [22], higher-order model checking have found applications in program analysis [20], and data compression [10].

1. Extensions of HOMC: beyond simple types (e.g. untyped and recursively typed recursion schemes, higher-type Böhm trees); beyond omega-regular properties: finitary parity, omega-B, stack unboundedness, etc.

2. “Practical” HOMC algorithms. E.g. HORSATZDD, Preface, C-SHORe, etc.

3. Applications of HOMC: program verification (functional, object-orientation, concurrency), program analysis, data compression, security, etc.

4. Higher-order grammars and pushdown automata. Context sensitivity of unsafe Maslov languages and other open problems.
5. Effective denotational semantics and strategy-aware models for HOMC. Compositional approaches to HOMC.

We plan to organize some of the following activities:

• Survey and tutorial lectures
• Technical presentations
• Panel / thematic discussions
• Open problems session
• Demos of software tools

[1] Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre. Recursion Schemes and Logical Reflection. In LICS, pages 120-129, 2010.

[2] Arnaud Carayol and Olivier Serre. Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection. In LICS, pages 165-174, 2012.

[3] Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible Pushdown Automata and Recursion Schemes. In LICS, pages 452-461, 2008.

[4] J. M. E. Hyland and C.-H. Luke Ong. On Full Abstraction for PCF: I, II and III. Information and Computation, 163(2):285-408, 2000.

[5] Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. TLCA, pages 253-267, 2001.

[6] Teodor Knapik, Damian Niwiński, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, pages 205-222, 2002.

[7] Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher- order programs. In POPL, page 416, January 2009.

[8] Naoki Kobayashi. Model Checking Higher-Order Programs. JACM, 60(3), 2013.

[9] Naoki Kobayashi and Atsushi Igarashi. Model-Checking Higher-Order Programs with Recursive Types. In ESOP, pages 431-450, 2013.

[10] Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi. Functional programs as compressed data. Higher-Order and Symbolic Computation, (2012):1-46, 2013.

[11] Naoki Kobayashi and C.-H. Luke Ong. A Type System Equivalent to the Modal Mu- Calculus Model Checking of Higher-Order Recursion Schemes. In LICS, pages 179-188, 2009.

[12] C.-H. Luke Ong. On Model Checking Trees Generated by Higher-Order Recursion Schemes. In LICS, pages 81-90, 2006.

[13] Pawe Parys. On the Significance of the Collapse Operation. In LICS, pages 521-530. IEEE, June 2012.

[14] Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. An Abstraction Refinement Approach to Higher-Order Model Checking. In POPL, pages 61-72, New York, USA, 2014. ACM Press.

[15] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In ICALP, pages 162-173, 2011.

[16] Sylvain Salvati and Igor Walukiewicz. Evaluation is MSOL-compatible. In FSTTCS, pages 103-114, 2013.

[17] Sylvain Salvati and Igor Walukiewicz. Using Models to Model-Check Recursive Schemes. In TLCA, pages 189-204, 2013.

[18] Sylvain Salvati and Igor Walukiewicz. Typing Weak MSOL Properties. In FoSSaCS, volume 7794, pages 129-144, 2015.

[19] Taku Terao and Naoki Kobayashi. A ZDD-Based Efficient Higher-Order Model.?? In APLAS, pages 354-371, 2014.

[20] Yoshihiro Tobita, Takeshi Tsukada, and Naoki Kobayashi. Exact flow analysis by higher- order model checking. FLOPS, pages 275-289, 2012.

[21] Takeshi Tsukada and C.-H. Luke Ong. Compositional Higher-order Model Checking via omega-Regular Games over Boehm trees. In CSL-LICS, 2014.

[22] Kazuhide Yasukata, Naoki Kobayashi, and Kazutaka Matsuda. Pairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model. In CONCUR, pages 312-326, 2014.