Résumé de mes activités et sujets de stages
Mots clés concernant mes principaux axes de recherche
preuves formelles, calcul formel, formalisation des mathématiques,
nombres réels, logique, théorie des types, vérification,
analyse numérique, spécifications formelles, raffinement,
systèmes d'aide à la preuve, ...
Quelques travaux
Mon outil d'aide à la preuve favori est
Rocq (anciennement 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 , des plus récents aux plus anciens (voir
les publications pour plus de détails):
- Développement d'une bibliothèque d'analyse numérique incluant l'intégrale de Lebesgue, des éléments finis, les théorèmes de Lax-Milgram, Tonelli... (en cours)
- Preuve formelle de l’algorithme CNDFS (en cours)
- L'outil de preuve interactif Coq et l'enseignement des maths dans le cadre du Défi Inria LiberAbaci (en cours)
- 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 des projets CerPAN et FOST
- Preuve formelle de raffinement de réseaux de Petri
- 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]
- Preuve formelle d'algorithme de différentiation automatique
- Développement de tactiques (automatisation de Coq et de PVS)
- Preuve formelle du théorème des trois intervalles
- Développement de la bibliothèque standard des nombres réels de Coq
- ...
Sujets de stage