En plus du séminaire de lundi (Maxime Lucas), nous aurons exceptionnellement un séminaire mardi par Pierre Vial. De par ses thématiques, ce séminaire sera commun avec celui de l’équipe Parsifal.

Résumé: The lambda-mu calculus [Parigot 92] is a computational interpretation of classical natural deduction, which extends the lambda-calculus. We first present non-idempotent intersection and union type systems characterizing head, weak and strong normalization in the lambda-mu calculus. 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, typability provides upper bounds for the lengths of the head, leftmost-outermost and maximal reduction sequences to normal form. Then, building on [Bernadet-Lengrand 13, Accatoli-Kesner-Lengrand 18], we refine these types system to statically obtain the exact measures of the lengths of these three strategies as well as the sizes of the computed normal forms. In contrast to the literature, we define a unique parametrized system, giving rise to optimally factorized proofs, which encapsulates the three evaluation paradigms/notions of normalization. This parametrized approach may be seen as a general methodological contribution to intersection (and union) type theory. The talk will begin with a gentle introduction to intersection type theory, in particular in the non-idempotent case.