Recent advances in higher-order automata and profinite lambda-calculus
Paul-André Melliès
Chair: Andreas Weiermann
In this talk, I will describe a number of recent advances at the converging point of automata theory, lambda-calculus and profinite topologies. The story starts with the observation made by Sylvain Salvati fifteen years ago that the notion of regular language of finite words and trees can be conservatively extended to the simply-typed lambda-calculus. A large part of my talk will be devoted to explaining how this idea connects to the Scott lattice semantics of linear logic, and how it can be extended to infinitary lambda-calculus and parity automata. I will in particular explain how the introduction of a \(\lambda Y_{\mu/\nu}\)-calculus with an inductive as well as a coinductive fixpoint operator leads to consider profinite topologies on lambda-terms, in connection with higher-order model checking.