Y. Bertot, Proving the convergence of a sequence based on algebraic-geometric means to ?, 2013.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Proceedings of the International Workshop on Types for proofs and programs (TYPES'06), pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013.
DOI : 10.1007/s10817-012-9255-4

URL : https://hal.archives-ouvertes.fr/hal-00649240

S. Boldo, C. Lelay, and G. Melquiond, Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP), pp.289-304, 2012.
DOI : 10.1007/978-3-642-35308-6_22

URL : https://hal.archives-ouvertes.fr/hal-00712938

S. Boldo, C. Lelay, and G. Melquiond, Formalization of real analysis: A survey of proof assistants and libraries. 2014. To be published in Mathematical Structures in Computer Science
URL : https://hal.archives-ouvertes.fr/hal-00806920

C. Cohen, Reasoning about big enough numbers in Coq, Proceedings of the 4th Coq Workshop

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, Proceedings of the 3rd International Conference of Mathematical Knowledge Management (MKM), pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

L. Cruz-filipe, A Constructive Formalization of the Fundamental Theorem of Calculus, Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'02), pp.108-126, 2003.
DOI : 10.1007/3-540-39185-1_7

M. Daumas, D. Lester, and C. Muñoz, Verified Real Number Calculations: A Library for Interval Arithmetic, IEEE Transactions on Computers, vol.58, issue.2, pp.226-237, 2009.
DOI : 10.1109/TC.2008.213

URL : https://hal.archives-ouvertes.fr/hal-00168402

B. Dutertre, Elements of mathematical analysis in PVS, Proceedings of the 9th International Conference Theorem Proving in Higher Order Logics (TPHOLs), pp.141-156, 1996.
DOI : 10.1007/BFb0105402

J. Fleuriot, On the mechanization of real analysis in, Proceeding of the 13th International Conference of Theorem Proving in Higher Order Logics (TPHOLs), volume 1869 of Lecture Notes in Computer Science, pp.145-161, 2000.

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

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'00), volume 2277 of Lecture Notes in Computer Science, pp.79-95, 2002.
DOI : 10.1007/3-540-45842-5_6

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

J. Harrison, Constructing the real numbers in HOL. Formal Methods in System Design, pp.35-59, 1994.

J. Harrison, . Hol, and . Light, Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp.60-66, 2009.
DOI : 10.1007/978-1-4302-0821-1_1

URL : https://hal.archives-ouvertes.fr/in2p3-00803620

J. Harrison, The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013.
DOI : 10.1007/s10817-012-9250-9

J. Hölzl, F. Immler, and B. Huffman, Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP), pp.279-294, 2013.
DOI : 10.1007/978-3-642-39634-2_21

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

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, pp.1-27, 2013.
DOI : 10.2168/LMCS-9(1:1)2013

C. Lelay, A new formalization of power series in Coq, 5th Coq Workshop, pp.1-2, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00880212

C. Lelay and G. Melquiond, Différentiabilité et intégrabilité en Coq Applicationàtion`tionà la formule de d'Alembert, 23èmes Journées Francophones des Langages Applicatifs, pp.119-133, 2012.

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

S. Mclaughlin and J. Harrison, A Proof-Producing Decision Procedure for Real Arithmetic, Proceedings of the 20th International Conference on Automated Deduction, pp.295-314, 2005.
DOI : 10.1007/11532231_22

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), pp.2-17, 2008.
DOI : 10.1007/978-3-540-71070-7_2

URL : https://hal.archives-ouvertes.fr/hal-00180138

C. Muñoz and A. Narkawicz, Formalization of Bernstein Polynomials and Applications to Global Optimization, Journal of Automated Reasoning, vol.43, issue.1, pp.151-196, 2013.
DOI : 10.1007/s10817-012-9256-3

A. Naumowicz and A. Korni?owicz, A Brief Overview of Mizar, Proceedings of the 22th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp.67-72, 2009.
DOI : 10.1007/3-540-44755-5_26

S. Owre, J. Rushby, and N. Shankar, PVS: A prototype verification system, Proceedings of the 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

O. Russell and . Connor, A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, vol.17, issue.1, pp.129-159, 2007.

O. Russell, B. Connor, and . Spitters, A computer-verified monadic functional implementation of the integral, Theoretical Computer Science, vol.411, issue.37, pp.3386-3402, 2010.

L. Pottier, Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics, Knowledge Exchange: Automated Provers and Proof Assistants, CEUR Workshop Proceedings, pp.67-76, 2008.

J. Rushby, S. Owre, and N. Shankar, Subtypes for specifications: predicate subtyping in PVS, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998.
DOI : 10.1109/32.713327

A. Trybulec, Some features of the Mizar language, Proceedings of the ESPRIT Workshop, 1993.

A. Trybulec, Non negative real numbers. Part I, Journal of Formalized Mathematics, 1998.