Colloque – Formalisation des mathématiques et types dépendants – Pierre-Marie Pédrot : Pour s’asseoir sur les fondations

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondationsPierre-Marie PédrotChargé de recherche, InriaRésuméLa preuve assistée par ordinateur séduit un public de plus en plus large. Jusque-là surreprésentée dans le domaine de l'informatique où elle était née, elle a commencé à susciter chez les mathématiciens un engouement certain. Néanmoins, cet appel d'air ne s'est pas fait sans incompréhension, les deux communautés ne partageant pas les mêmes arrière-fonds culturels.Cet exposé présente un point de vue informaticien assumé sur les fondements d'un assistant à la preuve et de la pertinence même de cette question. Notre thèse s'appuie sur l'équivalence preuve-programme, qui sera utilisée aussi bien comme paradigme théorique que comme approche sociologique. Notre vision est à la fois pluraliste et moniste. Moniste, car le choix d'une fondation a de nombreuses conséquences pratiques sur l'utilisation d'un assistant à la preuve, il faut donc concevoir le meilleur système. Pluraliste, car nous ne croyons pas en un langage unique des mathématiques : chaque sous-domaine s'exprime dans des langages extrêmement différents. Cette disparité est bien connue des informaticiens, qui utilisent de nombreux langages de programmation sur le même ordinateur. Cette tension est résolue via la compilation. Nous exposerons quelques techniques inspirées de ce domaine et évoquerons un avenir radieux où cohabitent pléthore de systèmes de preuve de haut niveau.Pierre-Marie PédrotPierre-Marie Pédrot est un chercheur en informatique spécialisé dans la théorie des types et est l'un des principaux développeurs de l'assistant à la preuve Rocq. Son travail s'articule autour du contenu calculatoire de la logique au travers de la correspondance preuve-programme. En s'inspirant de comportements venus du monde de la programmation appelés « effets de bord », il a notamment conçu des modèles de la théorie de types qui étendent sa puissance expressive. En complément de ce volet théorique, une partie importante de son activité consiste à implémenter et maintenir Rocq, avec une certaine emphase sur les questions de passage à l'échelle.