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
Completeness proofs for Kleene algebra
- Date
- Tuesday, January 15 2019 at 11:00AM
- Place
- Pavillon des Jardins
- Speaker
- Damien Pous (ENS Lyon)
Kleene algebra form a complete axiomatisation for regular expressions containments. This result was proved independently by Kozen and by Boffa and Krob in the early 90s. We will overview recent developments on such axiomatisation results, based on work with Amina Doumane, Anupam Das, and Paul Brunet. First we will present a new proof of completeness for Kleene algebra based on circular proof systems: sequent calculi where proofs are graphs rather than trees. Then we will discuss a natural extension of regular expressions, with an explicit intersection operator. This operator requires us to move from languages of words to languages of graphs ; we obtained a complete axiomatisation using an appropriate notion of graph automata.