Langage de programmation et compilateur formellement vérifié pour les bibliothèques numériques de bas niveau

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.