Documentation
Français (FR)

Anglais (EN)

Francois Clement

35

Documents

Publications

	Teaching Divisibility and Binomials with Coq Sylvie Boldo , François Clément , David Hamelin , Micaela Mayero , Pierre Rousselin RR-9547, Inria. 2024, pp.13 Rapport hal-04550762v1
	Lebesgue Induction and Tonelli's Theorem in Coq Sylvie Boldo , François Clément , Vincent Martin , Micaela Mayero , Houda Mouhcine [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17 Rapport hal-03564379v2
	A Coq Formalization of the Bochner integral Sylvie Boldo , François Clément , Louise Leclerc [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022 Rapport hal-03516749v2
	A Coq Formalization of Lebesgue Integration of Nonnegative Functions Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero [Research Report] RR-9401, Inria, France. 2021, pp.38 Rapport hal-03194113v2
	Lebesgue integration. Detailed proofs to be formalized in Coq François Clément , Vincent Martin [Research Report] RR-9386, Inria Paris. 2021, pp.567 Rapport hal-03105815v3
	The Lax–Milgram theorem. A detailed proof to be formalized in Coq François Clément , Vincent Martin [Research Report] RR-8934, Inria Paris. 2016 Rapport hal-01344090v2
	Deterministic Sensitivity Analysis for a Model for Flow in Porous Media Estelle Marchand , François Clément , Jean E. Roberts , Guillaume Pépin [Research Report] RR-6502, INRIA. 2008 Rapport inria-00271986v2
	Parallel Programming with the System Applications to Numerical Code Coupling François Clément , Roberto Di cosmo , Zheng Li , Vincent Martin , Arnaud Vodicka [Research Report] RR-5131, INRIA. 2004 Rapport inria-00071452v1
	Analyse de sensibilité et estimation de paramètres de transport pour une équation de diffusion, approche par état adjoint François Clément , Nina Khvoenkova , Alain Cartalade , Philippe Montarnal [Rapport de recherche] RR-5132, INRIA. 2004 Rapport inria-00071451v1
	Couplage de codes numériques, parallélisme et langages de haut niveau François Clément , Arnaud Vodicka , Roberto Di cosmo , Pierre Weis [Rapport de recherche] RR-4825, INRIA. 2003 Rapport inria-00071761v1
	Étude numérique du comportement de l'équation de transfert radiatif des milieux semi-transparents Inversion de données spectroscopiques pour le CO_2 Philippe Al khoury , Guy Chavent , François Clément , Philippe Hervé , Olivier Legras [Rapport de recherche] RR-4693, INRIA. 2003 Rapport inria-00071893v1
	Détermination de profils de température pendant la détonation d'un explosif liquide, le nitrométhane François Clément , Guy Chavent [Rapport de recherche] RR-4641, INRIA. 2002 Rapport inria-00071944v1
	The Inverse EEG and MEG Problems : The Adjoint State Approach I: The Continuous Case Olivier Faugeras , François Clément , Rachid Deriche , Renaud Keriven , Théodore Papadopoulo [Research Report] RR-3673, INRIA. 1999, pp.28 Rapport inria-00077112v1
	MBTT Inversion with a Poor Initial Velocity Background: Optimization Strategies? Density of Shots? François Clément [Research Report] RR-3657, INRIA. 1999 Rapport inria-00073016v1
	Migration-based Traveltime Waveform Inversion of 2D Simple Structures: the Synclay Model Guy Chavent , François Clément , Susana Gómez [Research Report] RR-3502, INRIA. 1998 Rapport inria-00073183v1
	Mise en oeuvre de la méthode MBTT pour un modèle acoustique par différences finies Guy Chavent , François Clément , Susana Gómez [Rapport de recherche] RR-2860, INRIA. 1996 Rapport inria-00073831v1
	Numerical Comparison of SVD and Propagator/Reflectivity Decomposition for the Acoustic Wave Equation Valery Khajdukov , Victor Kostin , Vladimir Tcheverda , François Clément , Guy Chavent [Research Report] RR-2888, INRIA. 1996 Rapport inria-00073802v1
	En route to waveform inversion by MBTT formulation : optimization for one shot and gradient for multiple shots Guy Chavent , François Clément , Susana Gomez [Research Report] RR-2150, INRIA. 1994 Rapport inria-00074523v1
	Waveform inversion through MBTT formulation Guy Chavent , François Clément [Research Report] RR-1839, INRIA. 1993 Rapport inria-00074833v1

	A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem Sylvie Boldo , François Clément , Vincent Martin , Micaela Mayero , Houda Mouhcine 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩ Communication dans un congrès hal-03889276v2
	Preuve formelle du théorème de Lax–Milgram Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France Communication dans un congrès hal-01581807v1
	A Coq formal proof of the Lax–Milgram theorem Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩ Communication dans un congrès hal-01391578v1
	Formal proof of a wave equation resolution scheme: the method error Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩ Communication dans un congrès inria-00450789v3
	Domain Decomposition and Skeleton Programming with OCamlP3l François Clément , Vincent Martin , Arnaud Vodicka , Roberto Di Cosmo , Pierre Weis Proceedings of the International Conference ParCo 2005, Sep 2005, France. pp.811-818 Communication dans un congrès hal-00149565v1
	Parameter identification for a one-dimensional blood flow model Jean-Frédéric Gerbeau , Vincent Martin , Astrid Decoene , François Clément CEMRACS 2004 - Centre d'été de Mathématiques et Recherche Avancées en Calcul scientifique : Mathematics and applications to biology and medicine, Jul 2004, Marseille, France. pp.174-200, ⟨10.1051/proc:2005014⟩ Communication dans un congrès hal-00700366v1

	A Coq Formalization of Lebesgue Integration of Nonnegative Functions Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩ Article dans une revue hal-03471095v1
	First-order indicators for the estimation of discrete fractures in porous media Hend Ben Ameur , Guy Chavent , Fatma Cheikh , François Clément , Vincent Martin Inverse Problems in Science and Engineering, 2018, 26 (1), pp.1--32. ⟨10.1080/17415977.2017.1290087⟩ Article dans une revue hal-01279503v2
	Les mathématiques s’appliquent aussi à l’industrie François Clément Interstices, 2017 Article dans une revue hal-01466798v1
	Trusting computations: a mechanized proof from partial differential equations to actual program Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond Computers & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩ Article dans une revue hal-00769201v3
	Wave equation numerical resolution: a comprehensive mechanized proof of a C program Sylvie Boldo , François Clément , Jean-Christophe Filliâtre , Micaela Mayero , Guillaume Melquiond Journal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩ Article dans une revue hal-00649240v3
	Image segmentation with multidimensional refinement indicators Hend Ben Ameur , Guy Chavent , François Clément , Pierre Weis Inverse Problems in Science and Engineering, 2011, Special Issue: Proceedings of the 5th International Conference on Inverse Problems: Modeling and Simulation, May 24th-29th, 2010, held in Antalya, Turkey, 19 (5), pp.577-597. ⟨10.1080/17415977.2011.579609⟩ Article dans une revue inria-00533799v3
	The multi-dimensional refinement indicators algorithm for optimal parameterization Hend Ben Ameur , François Clément , Pierre Weis , Guy Chavent Journal of Inverse and Ill-posed Problems, 2008, 16 (2), pp.107-126. ⟨10.1515/JIIP.2008.008⟩ Article dans une revue inria-00079668v6
	Shock-to-detonation transition of nitromethane: Time-resolved emission spectroscopy measurements Viviane Bouyer , Isabelle Ranc-Darbord , Philippe Hervé , Gérard Baudin , Christian Le Gallic Combustion and Flame, 2006, 144 (1-2), pp.139 - 150. ⟨10.1016/j.combustflame.2005.07.004⟩ Article dans une revue hal-01689514v1
	Domain decomposition and skeleton programming with OCamlP3l François Clément , Vincent Martin , Arnaud Vodicka , Roberto Di Cosmo , Pierre Weis Parallel Computing, 2006, 32 (7-8), pp.539-550. ⟨10.1016/j.parco.2006.04.003⟩ Article dans une revue hal-00149564v1

	OcamlP3l release 2.03 Roberto Di Cosmo , Pierre Weis , Francois Clement , Zheng Li 2007, ⟨swh:1:dir:85642a2e0333bbd6340c0a84ae6bad48cba11940;origin=https://hal.archives-ouvertes.fr/hal-02487579;visit=swh:1:snp:18b778c20ee37588bfa16bb8d00d8046bcbb462c;anchor=swh:1:rev:b34a952aad1b143e60e302df55a4f986ab904c42;path=/⟩ Logiciel hal-02487579v1