This one of the courses at the Lipa Summer School.
Slides: intro finite-mc lambda pushdowns-mc gfp-model ranked-lambda
A tree can represent all possible computations of a machine. For example, all computations of a finite automaton form a regular tree whose branching depends on the input letters. Rabin’s theorem implies that monadic second-order theory of a regular tree is decidable. What about trees generated by other devices?
In this series of lectures, we will present results and techniques for proving decidability of monadic second-order theories of trees generated by pushdown automata, lambda terms, and tree rewriting. These investigations bring intriguing questions about semantics, recognisability, and efficient algorithms for fixpoint
computation.