# LSV Seminar

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.

## Past Seminars

### A Curry-Howard Approach to Tree Automata

- Date
- Tuesday, June 13 2017 at 11:00AM
- Place
- Auditorium Daniel Chemla (Bât. Institut D'Alembert)
- Speaker
- Colin Riba (LIP, ENS Lyon)

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.