Programming language and formally verified compiler for low-level numerical libraries
Mardi 25 Novembre 2025 à 14h00 et visio
ENS Paris-Saclay, Salle 1Z76
Résumé : Les bibliothèques numériques de bas niveau telles que GMP et BLAS sont largement utilisées. Elles sont majoritairement écrites en C, Fortran ou assembleur et utilisent massivement des tableaux et des pointeurs. Ces langages sont adaptés à l'écriture de code efficace mais ne sont pas sûrs, c'est-à-dire qu'ils ont de nombreux comportements indéfinis qui augmentent le risque de bogues. De plus, leur sémantique rend difficile les raisonnements sur les programmes, et donc leur vérification ; il s'agit pourtant d'un point crucial car la correction des bibliothèques numériques est souvent subtile. Enfin, les compilateurs pour ces langages sont souvent très optimisants et donc très compliqués, ce qui peut limiter la confiance dans le code qu'ils génèrent.
Cette thèse porte sur la conception d'un langage, nommé Capla, et de son compilateur. Ceux-ci résolvent les problèmes précités tout en étant adaptés à l'écriture et à la vérification de bibliothèques numériques de bas niveau efficaces. En particulier, la sémantique de Capla, ainsi que les preuves de sûreté du langage et de correction du compilateur, ont été formalisées à l'aide de l'assistant de preuves Rocq.
The defense will be in English.
Jury:
- Arthur Charguéraud, Inria, Rapporteur et Examinateur
- Bas Spitters, Aarhus University, Rapporteur et Examinateur
- Gilles Barthe, Max Planck Institute, Examinateur
- Sandrine Blazy, Université de Rennes, Examinatrice
- Robbert Krebbers, Radboud University Nijmegen, Examinateur
- Xavier Leroy, Collège de France, Examinateur
- Mihaela Sighireanu, ENS Paris-Saclay, Examinatrice
- Guillaume Melquiond, Inria, Directeur de thèse