BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7156@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20181220T110000
DTEND;TZID=Europe/Paris:20181220T123000
DTSTAMP:20241120T203434Z
URL:https://www.i2m.univ-amu.fr/evenements/non-idempotent-typing-upper-bou
 nds-and-exact-length-in-the-lambda-and-in-the-lambda-mu-calculus/
SUMMARY:Pierre Vial (IRIF\, Université de Paris): Non idempotent typing\, 
 upper bounds and exact length in the lambda and in the lambda-mu-calculus
DESCRIPTION:Pierre Vial: Non-idempotent intersection type theory\, introduc
 ed independently by Gardner [94]\, Kfoury [96] and de Carvalho [07] arguab
 ly give the simplest to prove characterizations of semantical properties s
 uch as normalization (for various notions) or certifications of reduction 
 strategies. Moreover\, non-idempotent typing provides quantitative informa
 tion 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:\n-
 \n* 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\n-\n* Accattoli\, Kesner and Lengrand [ICFP2018] have 
 recently built on Bernadet-Lengrand work and obtained exact bounds for var
 ious strategies (head\, leftmost-outermost\, maximal) using non-idempotent
  types. I will explain how to refine this work and to statically obtain th
 e length of some strategies in the lambda-mu-calculus.\n-\nThe talk will b
 egin with a (hopefully) gentle introduction to non-idempotent typing and t
 he simply typed lambda-calculus.\n\nhttp://www.irif.fr/~pvial/
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Pierre_Vial.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20181028T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR