Floats and Ropes: A Case Study for Formal Numerical Program Verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009. ,
DOI : 10.1007/978-3-642-02930-1_8
Formal Proof of a Wave Equation Resolution Scheme: The Method Error, 1st Interactive Theorem Proving Conference (ITP), pp.147-162, 2010. ,
DOI : 10.1007/978-3-642-14052-5_12
URL : https://hal.archives-ouvertes.fr/inria-00450789
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Accepted for publication on, 2012. ,
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240
Formalization of the integral calculus in the PVS theorem prover, Journal of Formalized Reasoning, vol.2, issue.1, pp.1-26, 2009. ,
Constructive Real Analysis: a Type-Theoretical Formalization and Applications, 2004. ,
C-CoRN, the Constructive Coq Repository at Nijmegen, 3th International Conference on Mathematical Knowledge Management (MKM), pp.88-103, 2004. ,
DOI : 10.1007/3-540-45620-1_12
The definition of the Riemann definite integral and some related lemmas, Journal of Formalized Mathematics, vol.8, issue.1, pp.93-102, 1999. ,
On the mechanization of real analysis in, 13th International Conference on Theorem Proving in Higher Order Logics (TPHOL), pp.145-161, 2000. ,
Continuity and differentiability in ACL2 In: Computer-Aided Reasoning: ACL2 Case Studies, chap. 18, 2000. ,
Non-standard analysis in ACL2, Journal of Automated Reasoning, vol.27, issue.4, pp.323-351, 2001. ,
DOI : 10.1023/A:1011908113514
A small scale reflection extension for the Coq system, INRIA, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
Theorem Proving with the Real Numbers, 1998. ,
DOI : 10.1007/978-1-4471-1591-5
A HOL Theory of Euclidean Space, 18th International Conference on Theorem Proving in Higher Order Logics (TPHOL), pp.114-129, 2005. ,
DOI : 10.1007/11541868_8
Three chapters of measure theory in Isabelle/HOL, 2nd Interactive Theorem Proving Conference (ITP), pp.135-151, 2011. ,
Computing with classical real numbers, Journal of Formalized Reasoning, vol.2, issue.1, pp.27-39, 2009. ,
Différentiabilité et intégrabilité en Coq ApplicationàApplication`Applicationà la formule de d'Alembert, 23èmes Journées Francophones des Langages Applicatifs, pp.119-133, 2012. ,
Real function differentiability, Journal of Formalized Mathematics, vol.1, issue.4, pp.797-801, 1990. ,
Type classes for mathematics in type theory, Mathematical Structures in Computer Science, vol.2, issue.04, pp.795-825, 2011. ,
DOI : 10.1007/3-540-48256-3_10