R. D. Arthan, I. R. Boulton, and P. B. Jackson, An Irrational Construction of ??? from ???, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pp.43-58, 2001.
DOI : 10.1007/3-540-44755-5_5

J. Avigad and K. Donnelly, Formalizing O Notation in Isabelle/HOL, Proceedings of the 2nd International Joint Conference on Automated Reasoning of Lecture Notes in Computer Science, pp.357-371, 2004.
DOI : 10.1007/978-3-540-25984-8_27

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions, Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

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

M. Bickford, S. Boldo, F. Clément, J. Filliâtre, M. Mayero et al., Formalizing Constructive Analysis in Nuprl URL: http://www.nuprl.orgWave equation numerical resolution: a comprehensive mechanized proof of a C program, Journal of Automated Reasoning, vol.50, issue.4, pp.423-456, 2008.

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, pp.289-304, 2012.
DOI : 10.1007/978-3-642-35308-6_22
URL : https://hal.archives-ouvertes.fr/hal-00712938

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

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.

C. Byli´nskibyli´nski, Functions and their basic properties, Journal of Formalized Mathematics, vol.1, issue.1, pp.55-65, 1990.

A. Chaieb, Verifying Mixed Real-Integer Quantifier Elimination, Proceedings of the 3rd International Joint on Automated Reasoning, pp.528-540, 2006.
DOI : 10.1007/11814771_43

A. Chaieb, /. Isabelle, I. S. Hol, J. Autexier, J. Campbell et al., Parametric linear arithmetic over, Intelligent Computer Mathematics' Lecture Notes in Artificial Intelligence, vol.5144, pp.246-260, 2008.

A. Chaieb and M. Wenzel, Context Aware Calculation and Deduction, Proceedings of the 14th Symposium Calculemus 2007, pp.27-39, 2007.
DOI : 10.1007/978-3-540-73086-6_3

A. Ciaffaglione and P. Di-gianantonio, A certified, corecursive implementation of exact real numbers, Theoretical Computer Science, vol.351, issue.1, pp.39-51, 2006.
DOI : 10.1016/j.tcs.2005.09.061

C. Cohen, Formalized algebraic numbers: construction and first order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

J. R. Cowles and R. Gamboa, Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure, Proceeding of the 1st International Conference of Interactive Theorem Proving, pp.25-34, 2010.
DOI : 10.1007/978-3-642-14052-5_4

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

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, Proceedings of the 3rd International Conference of Mathematical Knowledge Management of Lecture Notes in Computer Science, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

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

D. Delahaye and M. Mayero, Field, une procédure de décision pour les nombres réels en Coq, Journées francophones des langages applicatifs, pp.33-48, 2001.

O. Desmettre, Coq standard library ? RiemannInt, 2002.

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

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.

N. Endou, K. Wasaki, and Y. Shidama, Definition of integrability for partial functions from R to R and integrability for continuous functions, Formalized Mathematics, vol.9, issue.2, pp.281-284, 2001.

J. Fleuriot, On the Mechanization of Real Analysis in Isabelle/HOL, Proceeding of the 13th International Conference of Theorem Proving in Higher Order Logics, pp.145-161, 2000.
DOI : 10.1007/3-540-44659-1_10

R. Gamboa, Continuity and differentiability in ACL2Computer-Aided Reasoning: ACL2 Case Studies', Advances in Formal Methods, pp.301-316, 2000.

R. Gamboa, J. R. Cowles, and N. Kuzmina, Axiomatic events in ACL2(r): A story of defun, defun-std, and encapsulate, Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and its Applications, 2004.

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

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Selected Papers of the International Workshop on Types for Proofs and Programs, pp.79-95, 2000.
DOI : 10.1007/3-540-45842-5_6

M. J. Gordon and T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, 1993.

H. Gottliebsen, Transcendental Functions and Continuity Checking in PVS, Proceedings of the 13th International Conference Theorem Proving in Higher Order Logics, pp.197-214, 2000.
DOI : 10.1007/3-540-44659-1_13

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, pp.98-113, 2005.
DOI : 10.1007/11541868_7

J. R. Guard, F. C. Oglesby, J. H. Bennett, and L. G. Settle, Semi-Automated Mathematics, Journal of the ACM, vol.16, issue.1, pp.49-62, 1969.
DOI : 10.1145/321495.321500

T. Hales, Dense Sphere Packings: A Blueprint for Formal Proofs, 2012.
DOI : 10.1017/CBO9781139193894

J. Harrison, Constructing the real numbers in HOL, Formal Methods in System Design, vol.98, issue.1-2, pp.35-59, 1994.
DOI : 10.1007/BF01384233

J. Harrison, Proof style, Lecture Notes in Computer Science, vol.1512, pp.154-172, 1996.
DOI : 10.1007/BFb0097791

J. Harrison, Floating point verification in HOL light: The exponential function, 1997.
DOI : 10.1007/BFb0000475

J. Harrison, A HOL Theory of Euclidean Space, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, pp.114-129, 2005.
DOI : 10.1007/11541868_8

J. Harrison, Towards Self-verification of HOL Light, Proceedings of the 3rd International Joint Conference, pp.177-191, 2006.
DOI : 10.1007/11814771_17

J. Harrison, Verifying Nonlinear Real Formulas Via Sums of Squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9

J. Harrison, HOL Light: An Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

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, pp.279-294, 2013.
DOI : 10.1007/978-3-642-39634-2_21

J. Hurd, The OpenTheory Standard Theory Library, Proceedings of the 3rd International Symposium on NASA Formal Methods, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76

J. Hölzl and A. Heller, Three Chapters of Measure Theory in Isabelle/HOL, Proceedings of the 2nd International Conference of Interactive Theorem Proving, pp.135-151, 2011.
DOI : 10.1017/CBO9780511810886

F. Immler and J. Hölzl, Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL, Proceedings of the 3rd International Conference on Interactive Theorem Proving, pp.377-392, 2012.
DOI : 10.1007/978-3-642-32347-8_26

C. Jones, Completing the rationals and metric spaces in LEGOPapers presented at the second annual Workshop on Logical environments, pp.297-316, 1993.

N. Julien and I. Pa¸scapa¸sca, Formal Verification of Exact Computations Using Newton???s Method, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, pp.408-423, 2009.
DOI : 10.1007/3-540-36126-X_17

L. S. Jutting, Checking Landau's " Grundlagen " in the AUTOMATH System, 1977.

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

M. Kaufmann, J. S. Moore, and P. Manolios, Computer-Aided Reasoning: An Approach, 2000.

J. Kotowicz, Convergent sequences and the limit of sequences, Journal of Formalized Mathematics, vol.1, issue.2, pp.273-275, 1990.

J. Kotowicz, Real sequences and basic operations on them, Journal of Formalized Mathematics, vol.1, issue.2, pp.269-272, 1990.

J. Kotowicz, The limit of a real function at a point, Journal of Formalized Mathematics, vol.2, issue.1, pp.71-80, 1991.

J. Kotowicz, The limit of a real function at infinity', Journal of Formalized Mathematics, vol.2, pp.17-28, 1991.

J. Kotowicz, One-side limits of a real function at a point, Journal of Formalized Mathematics, vol.2, issue.1, pp.29-40, 1991.

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

D. R. Lester, Topology in PVS, Proceedings of the second workshop on Automated formal methods , AFM '07, pp.11-20, 2007.
DOI : 10.1145/1345169.1345171

D. R. Lester, Real Number Calculations and Theorem Proving, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, pp.215-229, 2008.
DOI : 10.1007/978-3-662-21717-7

E. Makarov and B. Spitters, The Picard Algorithm for Ordinary Differential Equations in Coq, Proceeding of the 4th International Conference of Interactive Theorem Proving, pp.463-468, 2013.
DOI : 10.1007/978-3-642-39634-2_34

P. Manolios and J. S. Moore, Partial Functions in ACL2, Journal of Automated Reasoning, vol.31, issue.2, pp.107-127, 2003.
DOI : 10.1023/B:JARS.0000009505.07087.34

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

T. Mhamdi, O. Hasan, and S. Tahar, On the Formalization of the Lebesgue Integration Theory in HOL, Proceedings of the 1st International Conference of Interactive Theorem Proving, pp.387-402, 2010.
DOI : 10.1007/978-3-642-14052-5_27

D. Monniaux and P. Corbineau, On the Generation of Positivstellensatz Witnesses in Degenerate Cases, Proceedings of the 2nd International Conference on Interactive Theorem Proving, pp.249-264, 2011.
DOI : 10.1137/1038003
URL : https://hal.archives-ouvertes.fr/hal-00594761

J. S. Moore, T. Lynch, and M. Kaufmann, A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program, IEEE Transactions on Computers, vol.47, issue.9, pp.913-926, 1998.
DOI : 10.1109/12.713311

C. Muñoz and M. Mayero, Real automation in the field, 2001.

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. Narkawicz, C. Muñoz, and G. Dowek, Provably correct conflict prevention bands algorithms, Science of Computer Programming, vol.77, issue.10-11, pp.10-11, 2012.
DOI : 10.1016/j.scico.2011.07.002

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

O. Connor and R. , A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.129-159, 2007.
DOI : 10.1017/S0960129506005871

O. Connor and R. , Certified exact transcendental real number computation in Coq, Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics, pp.246-261, 2008.

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

S. Owre and N. Shankar, The PVS Prelude Library, 2003.

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

B. Perkowska, Functional sequence from a domain to a domain, Journal of Formalized Mathematics, vol.3, issue.1, pp.17-21, 1992.

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.

K. Raczkowski, Integer and rational exponents, Journal of Formalized Mathematics, vol.2, issue.1, pp.125-130, 1991.

P. Reid and R. Gamboa, Automatic Differentiation in ACL2, Proceeding of the 2nd International Conference of Interactive Theorem Proving, pp.312-324, 2011.
DOI : 10.1007/978-3-540-68942-3_3

S. Richter, Formalizing Integration Theory with an Application to Probabilistic Algorithms, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, pp.271-286, 2004.
DOI : 10.1007/978-3-540-30142-4_20

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

Z. Shi, W. Gu, X. Li, Y. Guan, S. Ye et al., The Gauge Integral Theory in HOL4, Journal of Applied Mathematics, vol.4, issue.1, 2013.
DOI : 10.1142/9789812810656

A. Solovyev and T. C. Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, Proceedings of the 5th NASA Formal Methods Symposium, pp.383-397, 2013.
DOI : 10.1007/978-3-642-38088-4_26

B. Spitters and E. Van-der-weegen, Type classes for mathematics in type theory, Mathematical Structures in Computer Science, vol.2, issue.04, pp.1-31, 2011.
DOI : 10.1007/3-540-48256-3_10

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 Addenda, 1998.

B. L. Vito, Strategy-enhanced interactive proving and arithmetic simplification for PVS, in 'Proceedings of STRATA 2003, First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, 2003.

M. Wenzel, Isabelle/Isar ? a versatile environment for human-readable formal proof documents, 2002.

M. Wenzel and F. Wiedijk, A comparison of the mathematical proof languages Mizar and Isar, Journal of Automated Reasoning, vol.29, issue.3/4, pp.389-411, 2002.
DOI : 10.1023/A:1021935419355

F. Wiedijk, The Seventeen Provers of the World, Lecture Notes in Artificial Intelligence, vol.3600, 2006.
DOI : 10.1007/11542384

F. Wiedijk, Statistics on digital libraries of mathematics', Studies in Logic, Grammar and Rhetoric, vol.18, issue.31, pp.137-151, 2009.