BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:6b12bda7-2f97-48a9-a771-2cf32a6cd3ac
X-WR-CALNAME:[MTV] Thibaut Benjamin (U. Cambridge) - Génération et automati
 sation de preuves d'identités en théorie des types dépendants
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20261025T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:6b12bda7-2f97-48a9-a771-2cf32a6cd3ac
DTSTAMP:20260425T162100Z
CLASS:PUBLIC
DESCRIPTION:Les assistants de preuves basés sur les types dépendants sont p
 armis les outils offrant les garanties les plus fortes sur la sécurité d'u
 n logiciel. Cependant\, pour des projets pratiques et de grande envergure\
 , ils induisent un effort de preuve conséquent limitant leur adoption. Une
  situation communément rencontrée est l'utilisation de types de données ef
 ficaces\, mais qui se prêtent peu au raisonnement\, rendant les preuves tr
 ès techniques. Une solution potentielle pour gérer cette complexité repose
  sur le principe d'univalence\, proposé par Voevodski\, qui postule que la
  bonne notion d'égalité entre les types est celles d'isomorphismes.  Ce pr
 incipe permet de transporter les algorithmes et leur preuves portant sur u
 n type de données se prêtant au raisonnement mais inefficace pour le calcu
 l vers un type de données efficace pour le calcul\, mais moins simple pour
  le raisonnement. Malheureusement\, le principe d'univalence est incompati
 ble avec celui d'unicité des preuves d'identités (UIP)\, un autre principe
  permettant souvent de simplifier les raisonnements. Cela signifie qu'en p
 ratique\, travailler avec le principe d'univalence nécessite de gérer les 
 preuves d'identités finement\, ce qui est complexe.  Dans cet exposé\, je 
 vais présenter  mes travaux et une direction de recherche pour simplifier 
 cette tache. Cette direction s'appuye sur un outil que je développe appelé
  CaTT\, permettant de décrire la structure algébrique des types d'identité
 s. Je montrerais comment le travail dans cet outil peut être partiellement
  automatisé\, et présenterai un plug-in de Coq permettant de générer des c
 alculs sur les termes d'identités. Cela permet de réduire l'effort de preu
 ve à fournir pour gérer les types d'identités. Par ailleurs l'incompatibil
 ité entre les deux principes implique qu'il n'est pas possible d'utiliser 
 simultanément une bibliothèque de preuves reposant l'univalence et une bib
 liothèque reposant sur UIP. En pratiques certaines utilisations de UIP son
 t cependant superflues\, et il est parfois possible de rendre deux telles 
 bibliothèques compatibles. Les travaux que je présenterai sont également u
 ne piste pour comprendre plus finement quand cela est possible et quel niv
 eau d'intervention humaine est requis pour réaliser cela.\n\n\nImport auto
 matique depuis https://framagenda.org/remote.php/dav/public-calendars/D3yq
 F7nwys9amfyY?export par sync_icals_to_drupal.py pour M2F
DTSTART;TZID=Europe/Paris:20241205T130000
DTEND;TZID=Europe/Paris:20241205T140000
LOCATION:LaBRI 178
SEQUENCE:0
SUMMARY:[MTV] Thibaut Benjamin (U. Cambridge) - Génération et automatisatio
 n de preuves d'identités en théorie des types dépendants
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
