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.
Seminar
Consuming and Persistent Typing for the Lambda-Mu Calculus
- Date
- 15.12.2020, 10:00
- Place
- online
- Speaker
- Pierre Vial (LMF)
In this talk, I will present a non-idempotent intersection and union type system, which characterizes exact measures of evaluation in the lambda-mu calculus of Parigot (a computational interpretation of classical natural deduction). In other words, for 3 evaluations strategies (head, leftmost-outer most and maximal, which are respectively associated to head, weak and strong normlaization), typing gives (1) the number of reduction steps to obtain the normal form and (2) the size of this normal form, for any normalizing term. Non-idempotent typing, inspired by Girard Linear Logic, gives a fine-grained control on duplication during reduction of programs and usually provides upper bounds for exacts measures of evaluation. By distinguishing type constructors depending on whether they are consuming (destroyed during evaluation) or persistent (remaining in normal forms) and building on previous work, we obtain exact bounds of evaluation. This is joint work with Delia Kesner. These results were presentend at Lics 2020. My talk will be just based on a knowledge of the simply typed lambda-calculus.