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.

Je m'intéresse aux problèmes inverses et aux techniques adjointes. En particulier, l'algorithme des indicateurs de raffinement qui construit une paramétrisation adaptative des quantités distribuées à identifier. Une application intéressante est la segmentation d'images.

Je m'intéresse maintenant principalement à l'utilisation de la programmation fonctionnelle pour le calcul scientifique, et plus particulièment au langage OCaml développé à l'Inria.
Je m'intéresse également à la preuve formelle de programmes de calcul scientifique. En particulier, je fais partie du projet MILC (DIM-RFSI 2018) qui concerne la formalisation en Coq de l'intégrale de Lebesgue. Ces travaux sont connexes à ceux effectués dans le cadre du GT ELFIC du Labex DigiCosme - Paris-Saclay, et font suite aux ANR CerPAN et Fost.

Logiciels

Sklml : the OCaml parallel skeleton system, un compilateur de squelettes de parallélisme fonctionnels et un système de programmation pour des programmes OCaml.
Ref-indic : Refinement indicators, une plateforme de paramétrisation adaptative par indicateurs de raffinement.
Ref-image : Image Segmentation by Refinement, segmentation d'images par des techniques de contrôle optimal.

Publications récentes

2022, S. Boldo, F. Clément, and L. Leclerc, A Coq Formalization of the Bochner integral, HAL.
2021, 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, à paraître, (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, 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 (pré-publié sur 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 14 janvier 2022.