The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
In this talk, I will present two equi-expressive models for generating infinite trees. The first one are higher-order recursion schemes, which can be thought as a deterministic rewriting system over terms (essentially, the simply-typed lambda calculus with recursion). The second one are higher-order pushdown automata, which are an extension of pushdown automata that uses stacks of stacks instead of stacks of symbols.
The first part of the talk will be devoted to present the models and give examples. The second part, will focus on properties of the trees generated by such models (in particular, the decidability of the monadic second order logic), and will illustrate the advantages of automata techniques when working with such objects.