CV Accueil - Archive ouverte HAL

	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
	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

	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
	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
	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
	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

	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

Sylvie Boldo