Évènement

Thibaut Benjamin
Cambridge
https://thibautbenjamin.github.io/

Date(s) : 12/09/2024   iCal
11h00 - 12h30

Dans cet exposé, je vais présenter une approche pour travailler avec
les types d’identité supérieurs en théorie des types homotopique, s’appuyant
sur un langage intermédiaire appelé CaTT modélisant les omega-catégories
faibles. Je vais d’abord présenter rapidement CaTT, puis montrer comment on
peut l’utiliser pour générer des types d’identité supérieurs. Finalement, je
montrerai comment il est possible d’utiliser des principes d’automatisation
pour CaTT, permettant de s’appuyer sur des principes simples pour générer en
quelques lignes des termes complexes, qui peuvent ensuite être utilisés pour
obtenir des résultats sur les identités supérieures.

Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories

• Séminaire