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:4868@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20230921T110000
DTEND;TZID=Europe/Paris:20230921T123000
DTSTAMP:20260107T155212Z
URL:https://www.i2m.univ-amu.fr/evenements/la-bicategorie-cartesienne-clos
 e-des-spans-fins/
SUMMARY:Simon Forest (LIS): La bicatégorie cartésienne close des spans fi
 ns
DESCRIPTION:Simon Forest: Dans le modèle Rel de la logique linéaire\, les
  types sont interprétés par des ensembles\, et les preuves/programmes pa
 r des relations. Une idée naturelle pour avoir un modèle quantitatif\, o
 u proof-relevant (c’est à dire que le modèle garde distinctes les diff
 érentes exécutions donnant lieu au même résultat observable)\, est d
 ’utiliser des spans au lieu de relations. En effet la (bi)catégorie Spa
 n\, dont les morphismes sont les spans d’ensembles composés par pullbac
 k\, peut-être vue comme un analogue “proof-relevant”: là où une rel
 ation entre A et B ne garde qu’une information binaire (si a et b sont e
 n relation)\, un span associe à tous a et b un ensemble de témoins\, ou 
 de “preuves” qu’ils sont en relation. Malheureusement\, une adaptati
 on naïve de l’exponentielle sur Rel ne fonctionne pas sur Span.\n\nD’
 autres travaux\, comme ceux sur les espèces de structure généralisées\
 , fournissent des modèles proof-relevant\, mais où la composition néces
 site un quotient complexe des témoins\, ne présentant ainsi pas l’aspe
 ct “concret” du pullback. Bien qu’un quotient semble inévitable\, u
 n autre modèle\, celui des “jeux concurrents fins”\, fait intervenir 
 une composition concrète\, sans quotient.\n\nAdaptant les techniques util
 isées dans ce dernier modèle\, ce travail donne de bons résultats dans 
 la direction d’un modèle de spans de LL\, où la composition se fait pa
 r des pullbacks classiques. On montre notamment que\, pour une pseudocomon
 ade adéquate sur les spans\, on obtient une bicatégorie de co-Kleisli ca
 rtésienne close.\n\nCeci est un travail en commun avec Pierre Clairambaul
 t.
CATEGORIES:Séminaire,Logique et Interactions
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