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, V. Martin, M. Mayero, and H. Mouhcine,
Lebesgue Induction and Tonelli's Theorem in Coq,
Rapport de Recherche
9457,
Inria.
- 2022, S. Boldo, F. Clément, and L. Leclerc,
A Coq Formalization of the Bochner integral,
Rapport de Recherche
9456,
Inria.
- 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 (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
(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 jeudi 10 février 2022.
© 1996-2022 INRIA, tous droits réservés.