Je m'intéresse aux preuves formelles et en particulier à
l'utilisation des systèmes d'aide à la preuve dans divers
domaines, avec lesquels il se développe des interactions, tels que le calcul
formel, les mathématiques,
la vérification, le hardware, les nombres réels et flottants, ...
Mon outil d'aide à la preuve favori est
Coq. J'ai effectué ma thèse
dans l'équipe qui
développe cet outil. Je l'utilise ou l'ai utilisé dans les
travaux suivants (voir les
publications pour
plus de détails):
- L'outil de preuve interactif Coq et l'enseignement des maths dans le cadre du Défi Inria LiberAbaci
- Mesure et Intégrale de Lebesgue en Coq dans le cadre du projet MILC
- Preuves de correction de bibliothèque d'éléments finis dans le
cadre du projet ELFIC
- Participation au projet Coquelicot (nouvelle bibliothèque de nombres réels en Coq)
- Développement de la bibliothèque CoqApprox dans le cadre du projet TaMaDi
- Preuve formelle de programme de combinatoire algébrique (logiciel SCHUR)
- Certification de
programmes d'analyse numérique dans le
cadre du projet
CerPAN que j'ai coordonné
et du projet FOST
- Preuve formelle de raffinement de réseaux
de Petri
- Preuve formelle du théorème des trois intervalles
- Utilisation dans le cadre de la différentiation automatique
- Développement de la bibliothèque des nombres réels de
Coq
- Développement de tactiques (automatisation de Coq et de
PVS)
- Interaction entre Coq et Maple
- Preuve formelle du 20ème problème de Diophante et
du théorème de Fermat pour n=4
[draft]
- ...
