Programming language and formally verified compiler for low-level numerical libraries
Tuesday 25 November 2025 at 14h00
ENS Paris-Saclay, Room 1Z76 and online
Abstract: Low-level numerical libraries like GMP and BLAS are widely used. They are mostly written in C, Fortran, and Assembly, and make a heavy use of arrays and pointers. These languages are well-suited for writing efficient code but they are not safe, that is, they have many undefined behaviors, which increase the chance for bugs. Moreover, their semantics make it difficult to reason about programs, and therefore to verify them; this is however a critical point because the correctness of numerical libraries is often subtle. Finally, the compilers for these languages are often very optimizing and thus very complex, which might reduce the confidence in the code they generate.
This thesis focuses on the design of a language, named Capla, and of its compiler. They address the aforementioned issues, while being well-suited to writing and verifying efficient low-level numerical libraries. In particular, the semantics of Capla, along with the proofs of type safety and of compiler correctness, have been formalized using the Rocq proof assistant.
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