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:5746@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230209T110000
DTEND;TZID=Europe/Paris:20230209T123000
DTSTAMP:20241120T200205Z
URL:https://www.i2m.univ-amu.fr/evenements/developpement-de-taylor-extensi
 onnel-des-%ce%bb-termes-purs/
SUMMARY:Lionel Vaux Auclair (I2M\, Aix Marseille université): Développeme
 nt de Taylor extensionnel des λ-termes purs
DESCRIPTION:Lionel Vaux Auclair: Né au début des années 2000 avec les tr
 avaux d’Ehrhard et Regnier sur le λ-calcul différentiel\, le développ
 ement de Taylor des programmes et des preuves est devenu un outil polyvale
 nt et un concept structurant pour l’étude du λ-calcul et de la logique
  linéaire.\nIl consiste à associer à chaque λ-terme un ensemble\, voir
 e une combinaison linéaire infinie de termes à ressources\, qui sont des
  approximations multilinéaires de λ-termes. Les termes à ressources son
 t eux-mêmes munis d’une dynamique\, qui est strictement finitaire (tous
  les termes sont fortement normalisables) et qu’on peut à son tour voir
  comme une approximation de la β-réduction : chaque pas de β-réduction
  est simulé par la réduction itérée des termes à ressources dans l’
 image du développement de Taylor. \nDans cet exposé\, je présenterai un
 e version extensionnelle du développement de Taylor : c’est-à-dire qu
 ’elle valide la règle η du λ-calcul\, qui assure que tout terme est 
 équivalent à une abstraction.\nLa prise en compte de la règle η est un
 e question naturelle (on sait très bien la gérer sur les arbres de Böhm
  par exemple)\, mais elle est étonnamment difficile. En effet\, contraire
 ment à la β-réduction\, elle ne peut pas se réduire à une transformat
 ion locale sur les termes à ressources du calcul introduit par Ehrhard et
  Regnier.\nLa solution\, issue de travaux en collaboration avec Lison Blon
 deau-Patissier et Pierre Clairambault\, consiste à considérer des termes
  à ressources qu’on peut qualifier d’η-longs. Dans un cadre typé\, 
 cette contrainte assure que tout terme de type fonctionnel est équivalent
  à une abstraction. En l’absence de typage\, on doit modifier la syntax
 e pour considérer des termes infiniment η-longs\, c’est-à-dire que ch
 aque valeur commence par une infinité d’abstractions. Je réserve les d
 étails scabreux de l’implémentation pour l’exposé mais les spécial
 istes de sémantique des jeux y trouveront des similitudes non fortuites.\
 nL’exposé sera également retransmis ici : https://greenlight.lal.clou
 d.math.cnrs.fr/b/lio-hdc-jef\n[su_spacer size="10"]\n\n\nSéminaire Logiqu
 e et Interactions\n&nbsp\;
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 023/01/Lionel_Vaux_Auclair-2023.png
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - Ancienne BU\, Salle Séminaire2 (RdC)\, 163 Avenue de
  Luminy\, 13009 Marseille\, France\, 
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, 1300
 9 Marseille\, France\, ;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - Ancienne B
 U\, Salle Séminaire2 (RdC):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20221030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR