Recursion schemes and the model checking of higher-order functional programs

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,
discuss implementations of these algorithms, and applications to the
model checking of higher-order functional programs.

Tuesday 19th October 2010, 14:00
Robert Recorde Room
Department of Computer Science