<p>Informatique et sciences numériques (2024-2025)</p><p>Thierry Coquand</p><p>Année 2024-2025</p><p>Chaire annuelle</p><p></p><p>Présentation de la chaire</p><p></p><p>Créée en partenariat avec Inria, la chaire annuelle Informatique et sciences numériques marque une volonté commune de faire valoir l'importance de cette discipline scientifique et la nécessité de lui octroyer une place pleine et entière.</p><p></p><p>Théorie des types dépendants et formalisation des mathématiques</p><p></p><p>La théorie des types a été introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l'on utilise de manière trop naïve la notion de collection d'objets. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves. Cette idée d'utiliser ainsi l'ordinateur connaît depuis quelques années un grand développement (vérification de la
