François Clément

You may prefer the English version.

Je suis chercheur au projet Serena, équipe commune au Centre de Recherche Inria (Paris) et au Cermics de l'École des Ponts ParisTech.

Domaines d'intérêt

Preuve formelle de programmes de calcul scientifique, avec le système Coq développé à l'Inria.
Application : formalisation de la méthode de éléments finis.
Ces travaux en cours sont connexes au projet MILC du DIM-RFSI (intégrale de Lebesgue) et au GT ELFIC du Labex DigiCosme - Paris-Saclay (théorème de Lax–Milgram),
et font suite aux ANR CerPAN et Fost (schéma aux différences finies pour l'équation des ondes).
Programmation fonctionnelle pour le calcul scientifique, avec le langage OCaml développé à l'Inria.
Application : compilateur de squelettes de parallélisme fonctionnels.
Problèmes inverses et techniques adjointes.
Application : algorithme des indicateurs de raffinement pour la construction d'une paramétrisation adaptative des quantités distribuées à identifier.

Logiciels

coq-num-analysis : Bibliothèque Coq d'analyse numérique, développements formels et preuves en Coq de problèmes d'analyse numérique.
Ref-image : Image Segmentation by Refinement, segmentation d'images par des techniques de contrôle optimal.
Ref-indic : Refinement indicators, une plateforme de paramétrisation adaptative par indicateurs de raffinement.
Sklml : the OCaml parallel skeleton system, un compilateur de squelettes de parallélisme fonctionnels et un système de programmation pour des programmes OCaml.

Publications récentes

2023, S. Boldo, F. Clément, V. Martin, M. Mayero, and H. Mouhcine, A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem, Proc. of the 25th Internat. Symp. on Formal Methods (FM 2023), pp. 39–55 [HAL] (pré-publié dans le Rapport de Recherche 9457, Inria).
2022, F. Clément, V. Martin, Lebesgue Integration. Detailed proofs to be formalized in Coq, Rapport de Recherche 9386 (rel2.0), Inria.
2022, S. Boldo, F. Clément, and L. Leclerc, A Coq Formalization of the Bochner integral, Rapport de Recherche 9456, Inria.
2022, S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq Formalization of Lebesgue Integration of Nonnegative Functions, Journal of Automated Reasoning, 66, pp. 175–213 [HAL] (pré-publié dans le Rapport de Recherche 9401, Inria).
2021, F. Clément, V. Martin, Lebesgue Integration. Detailed proofs to be formalized in Coq, Rapport de Recherche 9386 (rel1.1), Inria.
2018, H. Ben Ameur, G. Chavent, F. Cheikh, F. Clément, V. Martin, and J. E. Roberts, First-Order Indicators for the Estimation of Discrete Fractures in Porous Media, Inverse Problems in Science and Engineering, 26, pp. 1–32 (pré-publié dans le Rapport de Recherche 8857, Inria).
2017, S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq Formal Proof of the Lax–Milgram theorem, Proc. of the 6th ACM SIGPLAN Conf. on Certified Programs and Proofs (CPP 2017), pp. 79–89 [HAL].
2016, F. Clément, V. Martin, The Lax–Milgram Theorem. A detailed proof to be formalized in Coq, Rapport de Recherche 8934, Inria.
2014, S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, and P. Weis, Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program, Computers & Mathematics with Applications, 68, pp. 325–352 (pré-publié dans le Rapport de Recherche 8197, Inria).
2013, S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, and P. Weis, Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, 50, pp. 423–456 (pré-publié dans le Rapport de Recherche 7826, Inria).
2011, H. Ben Ameur, G. Chavent, F. Clément, and P. Weis, Image Segmentation with Multidimensional Refinement Indicators, Inverse Problems in Science and Engineering, 19, pp. 577–597 (pré-publié dans le Rapport de Recherche 7446, Inria).

Mon site perso (incluant quelques photos).

Malle : Francois.Clement@inria.fr.

URL : https://who.paris.inria.fr/Francois.Clement/
Auteur : François Clément
Dernière modification le vendredi 5 mai 2023.