IRIF, Université de Paris
Date(s) : 20/12/2018 iCal
11 h 00 min - 12 h 30 min
Non-idempotent intersection type theory, introduced independently by Gardner , Kfoury  and de Carvalho  arguably give the simplest to prove characterizations of semantical properties such as normalization (for various notions) or certifications of reduction strategies. Moreover, non-idempotent typing provides quantitative information on terms e.g. give upper bounds for the length of certain normalizing sequences. In this talk, I will present joint work with Delia Kesner:
* The extension of non-idempotent type theory to the lambda-mu-calculus, which is a computational interpretation of classical natural deduction. For this, we introduce non-idempotent union types. Typing then also gives upper bounds for the length of some normalizing sequences. This work was presented at FSCD17
* Accattoli, Kesner and Lengrand [ICFP2018] have recently built on Bernadet-Lengrand work and obtained exact bounds for various strategies (head, leftmost-outermost, maximal) using non-idempotent types. I will explain how to refine this work and to statically obtain the length of some strategies in the lambda-mu-calculus.
The talk will begin with a (hopefully) gentle introduction to non-idempotent typing and the simply typed lambda-calculus.