Decidability of extensions of recursion schemes via intersection types

Steven Ramsay

Higher-order recursion schemes (HORS) are a class of higher-order programs which are equivalent in expressive power to terms of the simply typed lambda calculus with recursion and first-order, uninterpreted constants. Since the trees that they define have many decidable properties, they have become widely studied in connection with the verification of functional programs through higher-order model checking.

In this talk, I will review the intersection type characterisation of higher-order model checking due to Kobayashi (POPL'09) and then present a new semantic framework that subsumes it. In this framework, recursion schemes can be extended by new, interpreted constants that are modelled concretely as a continuous function over domains and abstractly as an intersection type. When the intersection type of each constant is shown to be an exact abstract interpretation of the concrete semantics of that constant then intersection type assignment will characterise property checking for arbitrary terms. Since we focus on finite intersection type systems, decidability is a corollary.