Recursion Schemes, Types and ModelChecking Functional Programs
Prof. Luke Ong ( Oxford University Computing Laboratory )

16:30 28th April 2009 ( week 1, Trinity Term 2009 )Lecture Theatre B
Recursion schemes are in essence the simplytyped lambda calculus with recursion, generated from firstorder 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 higherorder 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 secondorder theories, and the graphs have decidable modal mucalculus theories.
In a POPL09 paper, Kobayashi shows that verification problems (such as resource usage, safety properties, and flow analysis) of higherorder 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 typetheoretic characterisations of highly complex theories, so that (for example) the modal mucalculus model checking of ordern recursion schemes is reducible to a problem of typability of recursion schemes, which we show is decidable (nEXPTIME complete). These type theories are simple to define; preliminary results show that the typechecking 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.
In a POPL09 paper, Kobayashi shows that verification problems (such as resource usage, safety properties, and flow analysis) of higherorder 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 typetheoretic characterisations of highly complex theories, so that (for example) the modal mucalculus model checking of ordern recursion schemes is reducible to a problem of typability of recursion schemes, which we show is decidable (nEXPTIME complete). These type theories are simple to define; preliminary results show that the typechecking 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.