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:6266@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20211118T160000
DTEND;TZID=Europe/Paris:20211118T170000
DTSTAMP:20241209T162531Z
URL:https://www.i2m.univ-amu.fr/evenements/sur-la-syntaxe-de-la-semantique
 -quantitative-hdr-lionel-vaux-auclair/
SUMMARY:Lionel Vaux Auclair (I2M\, Aix-Marseille Université): Sur la synta
 xe de la sémantique quantitative
DESCRIPTION:Lionel Vaux Auclair: Composition du jury\n\n 	Robin Cockett (Ca
 lgary\, rapporteur)\,\n 	Ugo Dal Lago (Bologna)\,\n 	Delia Kesner (Paris\,
  rapporteuse)\,\n 	Guy McCusker (Bath\, rapporteur)\,\n 	Paul-André Melli
 ès (Paris)\,\n 	Myriam Quatrini (Aix-Marseille)\,\n 	Laurent Regnier (Aix
 -Marseille).\n\nRésumé\nLe développement de Taylor des λ-termes et des
  preuves de la logique linéaire est le fruit d’une relecture syntaxique
  par Ehrhard et Regnier de la sémantique quantitative de Girard : il as
 socie à chaque terme ou preuve une combinaison linéaire infinie d’appr
 oximations multilinéaires et finies de l’objet de départ. Il matérial
 ise une correspondance étroite entre le comportement calculatoire des ter
 mes\, défini par la β-réduction\, et leur interprétation dans certains
  modèles dénotationnels : le développement de Taylor d’un terme est
  toujours normalisable\, et sa forme normale correspond exactement à l’
 arbre de Böhm du terme. Cette correspondance se retrouve dans le fait que
 \, pour de nombreux modèles de la logique linéaire\, la promotion d’un
  morphisme s’obtient comme une superposition d’opérations multilinéa
 ires\, faisant du développement de Taylor des preuves une structure sous-
 jacente de ces modèles.\nCe mémoire présente quelques avancées récent
 es visant à raffiner l’analyse de la normalisation (qui est un processu
 s potentiellement infini) offerte par le développement de Taylor pour la 
 ramener au niveau de la β-réduction ou de l’élimination des coupures 
 (qui correspond à un calcul fini).\nOn démontre que cette approche perme
 t d’étendre l’analyse à un cadre non-uniforme\, susceptible de prend
 re en compte par exemple une forme de non-déterminisme calculatoire — a
 lors que la normalisation peut échouer dans ce cadre. On démontre égale
 ment que la même approche peut être appliquée aux réseaux de démonstr
 ation de la logique linéaire. Enfin les techniques développées précéd
 emment permettent de revisiter et simplifier le résultat originel d’Ehr
 hard et Regnier pour la normalisation dans le cas uniforme\, tout en l’a
 daptant à une forme restreinte de non-déterminisme.\n\nLa soutenance ser
 a précédée d’une séance du séminaire logique et interactions\, à 1
 4h et toujours à la FRUMAM\, avec deux exposés donnés l’un par Ugo Da
 l Lago et l’autre par Paul-André Melliès.
CATEGORIES:Soutenance d'HdR,AGLR,Logique et Interactions
LOCATION:Saint-Charles - FRUMAM (3ème étage)\, 3\, place Victor Hugo\, Ma
 rseille\, 13003\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=3\, place Victor Hugo\, Mar
 seille\, 13003\, France;X-APPLE-RADIUS=100;X-TITLE=Saint-Charles - FRUMAM 
 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20211031T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR