(Oxford)

Recursion schemes are in essence the simply-typed lambda calculus withrecursion, 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,

discuss implementations of these algorithms, and applications to the

model checking of higher-order functional programs.

Robert Recorde Room

Department of Computer Science