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.