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 projectteam between
Inria (Paris)
Center and Cermics from
École des Ponts ParisTech.
Fields of interest
 Formal proof for scientific computing programs, with the
Coq system developed at Inria.
Application: formalization of the finite element method.
These works are related to those of the
MILC project from DIMRFSI
(Lebesgue integral) and of the
ELFIC working group
from Labex DigiCosme  ParisSaclay (Lax–Milgram theorem),
and follow the former ANR projects
CerPAN and
Fost (finite difference scheme
for the wave equation).
 Functional programming for scientific computation, with the
OCaml language developed at Inria.
Application: functional parallel skeleton compiler.
 Inverse problems and adjoint techniques.
Application: refinement indicators algorithm to build an adaptive
parameterization of the distributed quantities to be identified.
Software

coqnumanalysis :
Numerical analysis Coq library,
formal developments and proofs in Coq of numerical analysis problems.
 Refimage:
Image Segmentation by Refinement,
image segmentation using optimal control techniques.
 Refindic:
Refinement indicators,
an adaptive parameterization platform using refinement indicators.
 Sklml:
the OCaml parallel skeleton system,
a functional parallel skeleton compiler and programming system for OCaml
programs.
Recent publications
 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]
(prepublished in Research Report
9457,
Inria).
 2022, F. Clément, V. Martin,
Lebesgue Integration. Detailed proofs to be formalized in Coq,
Research Report
9386 (rel2.0),
Inria.
 2022, S. Boldo, F. Clément, and L. Leclerc,
A Coq Formalization of the Bochner integral,
Research Report
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]
(prepublished in Research Report
9401,
Inria).
 2021, F. Clément, V. Martin,
Lebesgue Integration. Detailed proofs to be formalized in Coq,
Research Report
9386 (rel1.1),
Inria.
 2018, H. Ben Ameur, G. Chavent, F. Cheikh, F. Clément, V. Martin, and
J. E. Roberts,
FirstOrder Indicators for the Estimation of Discrete Fractures in
Porous Media,
Inverse
Problems in Science and Engineering,
26, pp. 1–32
(prepublished in Research 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
[HAL].
 2016, F. Clément, V. Martin,
The Lax–Milgram Theorem.
A detailed proof to be formalized in Coq,
Research 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
(prepublished in Research 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
(prepublished in Research 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
(prepublished in Research Report
7446,
Inria).
My personal web site (in French, but
including some pictures).
Email: Francois.Clement@inria.fr.
URL: https://who.paris.inria.fr/Francois.Clement/index.en.htm
Author: François Clément
Last modification on Friday, May 5th, 2023.
© 19962023 INRIA, all rights reserved.