François Clément
Vous préférez peut-être la version française.
I am a research scientist in the
Serena group,
a joint project-team between
Inria (Paris)
Center and Cermics from
École des Ponts ParisTech.
My domains of interests are inverse problems and adjoint techniques.
In particular, the refinement indicators algorithm which builds an adaptative
parameterization of the distributed quantities to be identified.
An interesting application is image segmentation.
Now, my main domain of interest is the use of functional programming for
scientific computation, and more precisely to the
OCaml language
developed at Inria.
I am also interested in formal proof for scientific computing programs.
I am a member of the MILC
project (DIM-RFSI 2018) that deals with the formalization in Coq of the
Lebesgue integral.
These works are related to those of the
ELFIC working group
from Labex DigiCosme - Paris-Saclay, and follow the former ANR projects
CerPAN
and Fost.
Software
- Sklml:
the OCaml parallel skeleton system,
a functional parallel skeleton compiler and programming system for OCaml
programs
(easy coarse grain parallelization).
- Ref-indic:
Refinement indicators,
an adaptive parameterization platform using refinement indicators
(details only where they are worth it).
- Ref-image:
Image Segmentation by Refinement,
image segmentation using optimal control techniques
(no gestalt inside).
Recent publications
- 2021, F. Clément, V. Martin,
Lebesgue Integration. Detailed proofs to be formalized in Coq,
Technical Report
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
(pre-published in Technical Report
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
(pre-published on HAL).
- 2016, F. Clément, V. Martin,
The Lax-Milgram Theorem. A detailed proof to be formalized in Coq,
Technical Report
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
(pre-published in Technical Report
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
(pre-published in Technical Report
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
(pre-published in Technical Report
7446,
Inria).
My personal web site (in French, but
including some pictures).
E-mail: Francois.Clement@inria.fr.
URL: https://who.paris.inria.fr/Francois.Clement/index.en.htm
Author: François Clément
Last modification on Sunday, February 7th, 2021.
© 1996-2021 INRIA, all rights reserved.