BLC 2010

Recursion schemes and the model checking of higher-order computation
Luke Ong
Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. An old model of computation much studied in the 70's, there has been a revival of interest in recursion schemes as generators of rich infinite structures (such as infinite trees) for modelling higher-order computation. In this talk we will survey recent proofs of the decidability of monadic second order theories of these structures, and discuss applications to the verification of higher-order programs.