Thursday 12 December 2019, 14:00, LSV library: Capturing exact measures of evaluation with non-idempotent types in classical natural deduction, Pierre Vial (Post-doc, Galinette).

In this talk, we will show how non-idempotent intersection types can *statically* capture *exact measures* of terms in the lambda-mu calculus [Parigot 92], which is a computational interpretation of *classical* natural deduction extending the intuitionistic lambda-calculus. By exact measures, we mean both the number of evaluation steps to the normal form, and its size. The non-idempotent* approach [Gardner 94, de Carvalho 07] provides very simple combinatorial arguments –based on decreasing measures of type derivations– to characterize head and strongly normalizing terms. Moreover, in this setting, typability provides *upper bounds* for the lengths of evaluation and size of the normal form.

Building on [Bernadet-Lengrand 13, Accatoli-Kesner-Lengrand 18], we refine a non-idempotent intersection and union type system to statically obtain the *exact measures* associated to head, weak and strong normalization in the lambda-mu calculus. We do so in a parametrized way (we use a unique type system for the three notions of normalization).

The talk will begin with a gentle introduction to intersection type theory, in particular in the non-idempotent case.