S. Boldo, 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

S. Boldo, F. Clément, J. C. Filliâtre, M. Mayero, G. Melquiond et al., 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

S. Boldo, F. Clément, J. C. Filliâtre, M. Mayero, G. Melquiond et al., 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

R. W. Butler, Formalization of the integral calculus in the PVS theorem prover, Journal of Formalized Reasoning, vol.2, issue.1, pp.1-26, 2009.

L. Cruz-filipe, Constructive Real Analysis: a Type-Theoretical Formalization and Applications, 2004.

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, 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

N. Endou and A. Korni-lowicz, The definition of the Riemann definite integral and some related lemmas, Journal of Formalized Mathematics, vol.8, issue.1, pp.93-102, 1999.

J. Fleuriot, On the mechanization of real analysis in, 13th International Conference on Theorem Proving in Higher Order Logics (TPHOL), pp.145-161, 2000.

R. Gamboa, Continuity and differentiability in ACL2 In: Computer-Aided Reasoning: ACL2 Case Studies, chap. 18, 2000.

R. Gamboa and M. Kaufmann, Non-standard analysis in ACL2, Journal of Automated Reasoning, vol.27, issue.4, pp.323-351, 2001.
DOI : 10.1023/A:1011908113514

G. Gonthier, A. Mahboubi, and E. Tassi, A small scale reflection extension for the Coq system, INRIA, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

J. Harrison, Theorem Proving with the Real Numbers, 1998.
DOI : 10.1007/978-1-4471-1591-5

J. Harrison, 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

J. Hölzl and A. Heller, Three chapters of measure theory in Isabelle/HOL, 2nd Interactive Theorem Proving Conference (ITP), pp.135-151, 2011.

C. Kaliszyk and R. O-'connor, Computing with classical real numbers, Journal of Formalized Reasoning, vol.2, issue.1, pp.27-39, 2009.

C. Lelay and G. Melquiond, 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.

K. Raczkowski and P. Sadowski, Real function differentiability, Journal of Formalized Mathematics, vol.1, issue.4, pp.797-801, 1990.

B. Spitters and E. Van-der-weegen, 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