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:4796@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230525T110000
DTEND;TZID=Europe/Paris:20230525T123000
DTSTAMP:20260107T160745Z
URL:https://www.i2m.univ-amu.fr/evenements/caracterisation-de-h-par-le-dev
 eloppement-de-taylor-extensionnel/
SUMMARY:Lionel Vaux-Auclair (I2M): Caractérisation de H* par le développe
 ment de Taylor extensionnel
DESCRIPTION:Lionel Vaux-Auclair: Le développement de Taylor extensionnel d
 éjà présenté au séminaire\nle 9 février dernier valide les règles 
 β et η : deux termes\nβη-convertibles ont des développements de Tayl
 or équivalents (pour la\nréduction du calcul à ressources extensionnel)
 .\n\nMieux : comme les sémantiques des jeux dont il est inspiré\, ce\nd
 éveloppement de Taylor extensionnel est un modèle de la théorie H*\,\nl
 a plus grande λ-théorie cohérente et sensée. Celle-ci peut être\ncara
 ctérisée par l’égalité des arbres de Nakajima\, qui sont des sortes\
 nd’arbres de Böhm infiniment η-longs (c’est un exercice du Barendreg
 t)\,\nmais ces derniers sont difficiles à définir et à manipuler. On pe
 ut\nvoir le calcul à ressources extensionnel comme un langage\nd’approx
 imations finies des arbres de Nakajima\, à la syntaxe et à la\ndynamique
  très simples\, au même titre que le calcul à ressources\nusuel défini
 t un calcul d’approximations finies des arbres de Böhm.\n\nDans cet exp
 osé\, je rappellerai rapidement la syntaxe du calcul à\nressources exten
 sionnel et les propriétés basiques du développement de\nTaylor associé
 . Je démontrerai ensuite que deux λ-termes ont des\ndéveloppements de T
 aylor extensionnels équivalents ssi ils sont\néquivalents pour H*. J’e
 xpliquerai enfin comment ce résultat permet\nd’établir simplement qu
 ’un certain modèle relationnel du λ-calcul\nadmet H* comme théorie (u
 n résultat de Manzonetto\, dont la\ndémonstration se ramène maintenant 
 au seul fait que ce modèle est\ncompatible avec le développement de Tayl
 or extensionnel).\n\nComme le précédent\, cet exposé est basé sur des 
 travaux en cours\navec Lison Blondeau-Patissier (qui en abordera d’autre
 s aspects le 22\njuin) et Pierre Clairambault. Les prépublications sont l
 à :\n\nhttps://arxiv.org/abs/2302.04685 et https://arxiv.org/abs/2305.084
 89.
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:DAYLIGHT
DTSTART:20230326T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR