Non idempotent typing, upper bounds and exact length in the lambda and in the lambda-mu-calculus
Pierre Vial
IRIF, Université de Paris
https://pierrevial.github.io/
Date(s) : 20/12/2018 iCal
11h00 - 12h30
Non-idempotent intersection type theory, introduced independently by Gardner [94], Kfoury [96] and de Carvalho [07] 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.
Catégories
