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

Visit website for this news | Export event in iCalendar format

 Frédéric Blanqui
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.)


About LSV

Agenda

Export agenda in iCalendar format | Past seminars

Tue, Jan 22
Tue, Jan 29
Tue, Feb 5
Tue, Feb 19

Past seminars