Recursion Schemes, Types and Model-Checking Functional Programs
Luke Ong (Oxford)
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 (called recursive program schemes at the time), there has been a revival
of interests in higher-order recursion schemes as generators of infinite hierarchies of infinite structures
such as word languages, trees and graphs. These structures are robust: as definitional devices, recursion schemes are equivalent
to a new type of higher-order pushdown automata called collapsible pushdown automata.
Much is also now known about their rich algorithmic properties: 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 n-EXPTIME complete. Remarkably these type theories are very simple to define;
and preliminary results show that the type-checking procedures work well in practice, despite the high complexity.
In this talk, I will survey the algorithmic model theory of recursion schemes,
and the application to the model checking of functional programs.