Non idempotent typing, upper bounds and exact length in the lambda and in the lambda-mu-calculus

Pierre Vial
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 [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.


Retour en haut 

Secured By miniOrange