Amphithéâtre Guillaume Budé, Site Marcelin Berthelot
En libre accès, dans la limite des places disponibles
-

Résumé

Le dernier séminaire a conclu la série par une perspective personnelle sur l’histoire et l’actualité de la théorie des types. Le conférencier est revenu sur son invention avec Huet du calcul des constructions, le formalisme à la base de l’assistant de preuves Coq. Le calcul des constructions est apparu comme une synthèse entre les travaux de de Bruijn sur le système Automath pour la mécanisation des mathématiques, les travaux de Girard sur le système Fω, et les travaux de Martin-Löf sur sa théorie des types. Ces formalismes débouchent aujourd’hui sur une approche nouvelle et prometteuse de la notion mathématique d’identification entre deux collections, généralisant les notions d’isomorphismes entre structures algébriques et de transport de propriétés.

Intervenants

Thierry Coquand