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
Computability path ordering
- Date
- Tuesday, January 13 2015 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Frédéric Blanqui (INRIA Paris-Rocquencourt)
We study here the computability path ordering (CPO), aiming at carrying out termination proof for higher-order calculi. CPO appears to be the ultimate improvement of the higher-order recursive path ordering (HORPO) in the sense that this definition captures the essence of computability arguments à la Tait and Girard, therefore explaining the name of the improved ordering. We show that CPO allows to consider higher-order rewrite rules in a simple type discipline with inductive types, that most of the guards present in the recursive calls of its core definition cannot be relaxed in any natural way without loosing well-foundedness, and that the precedence on function symbols cannot be made more liberal anymore.
(Joint work with J.-P. Jouannaud and A. Rubio.)