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:5328@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20240912T110000
DTEND;TZID=Europe/Paris:20240912T123000
DTSTAMP:20240905T090306Z
URL:https://www.i2m.univ-amu.fr/evenements/tba-156/
SUMMARY:Thibaut Benjamin (Cambridge): Automatisation des calculs dans les c
 atégories supérieures et génération de preuves d'égalités
DESCRIPTION:Thibaut Benjamin: Dans cet exposé\, je vais présenter une app
 roche pour travailler avec\nles types d'identité supérieurs en théorie 
 des types homotopique\, s'appuyant\nsur un langage intermédiaire appelé 
 CaTT modélisant les omega-catégories\nfaibles. Je vais d'abord présente
 r rapidement CaTT\, puis montrer comment on\npeut l'utiliser pour génére
 r des types d'identité supérieurs. Finalement\, je\nmontrerai comment il
  est possible d'utiliser des principes d'automatisation\npour CaTT\, perme
 ttant de s'appuyer sur des principes simples pour générer en\nquelques l
 ignes des termes complexes\, qui peuvent ensuite être utilisés pour\nobt
 enir des résultats sur les identités supérieures.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20240331T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR