François Clément's Home Page

Vous préférez peut-être la version française.

I look like this! Well, not everyday...
I am a research scientist in the Serena group, a joint team between Inria Paris Center and University Paris-Est, Cermics (ENPC).
I am the Inria-Enterprises correspondent of the Inria Research Center of Paris for AMIES.

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 ELFIC working group from Labex DigiCosme - Paris-Saclay that deals with the proof of correctness of a C++ library for the finite element method. These works follow 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

2016, 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 (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).

I also have a personal web site (mostly in French).

E-mail: Francois.Clement@inria.fr.

URL: http://who.rocq.inria.fr/Francois.Clement/index.en.htm
Author: François Clément
Last modification date: Thursday, May 25th, 2017.

The content of these pages comes under the only responsibility of their author, and does not necessarily represent the official point of view of INRIA. Information is presented in all sincerity, but its correctness could not be guaranteed.