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.
This talk surveys a Curry-Howard perspective on Rabin's Tree Theorem, the decidability of Monadic Second-Order Logic (MSO) on infinite trees.
Rabin's Tree Theorem proceeds by effective translations of MSO-formulae to tree automata. The operations on tree automata used in these translations can be organized in a deduction system based on intuitionistic linear logic (ILL). We propose a computational interpretation of this deduction system along the lines of the Curry-Howard proofs-as-programs correspondence. Relying on the usual technology of game semantics, we interpret proofs as strategies in two-player games generalizing usual acceptance games of tree automata.
This realizability semantics satisfies an expected property of witness extraction from proofs of existential statements. It also allows to combine realizers produced as interpretations of proofs with strategies witnessing (non-)emptiness of tree automata, possibly obtained using external algorithms. Moreover, an adaptation of a usual construction for the simulation of alternating automata by non-deterministic ones satisfies the deduction rules of the "of course" exponential modality of ILL.