Recursion Schemes, Types and Model-Checking Functional Programs

Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from first-order function symbols. An old model of computation much studied in the 70's, recursion schemes have enjoyed a revival of interests as generators of remarkably rich hierarchies of infinite structures such as word languages, infinite trees and graphs. These structures are robust: as a definitional device, recursion schemes are equivalent to a new type of higher-order pushdown automata called collapsible pushdown automata. Much is also now known about their strong algorithmic properties which are highly relevant to verification: the trees have decidable monadic second-order theories, and the graphs have decidable modal mu-calculus theories.

In a POPL09 paper, Kobayashi shows that verification problems (such as resource usage, safety properties, and flow analysis) of higher-order functional programs can easily be reduced to model checking problems of recursion schemes. In recent joint work with Kobayashi, we use a kind of refined intersection types to construct type-theoretic characterisations of highly complex theories, so that (for example) the modal mu-calculus model checking of order-n recursion schemes is reducible to a problem of typability of recursion schemes, which we show is decidable (n-EXPTIME complete). These type theories are simple to define; preliminary results show that the type-checking procedures work well in practice.

In this talk, I will survey the algorithmic model theory of recursion schemes, and review recent progress, including the novel application to the model checking of functional programs.