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.

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 DIM-RFSI (Lebesgue integral) and of the ELFIC working group from Labex DigiCosme - Paris-Saclay (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

coq-num-analysis : Numerical analysis Coq library, formal developments and proofs in Coq of numerical analysis problems.
Ref-image: Image Segmentation by Refinement, image segmentation using optimal control techniques.
Ref-indic: 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] (pre-published 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] (pre-published 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, 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 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 (pre-published 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 (pre-published 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 (pre-published in Research 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 Friday, May 5th, 2023.