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

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pa¸scapa¸sca, Canonical Big Operators, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, 2008.
DOI : 10.1007/3-540-44659-1_29

URL : https://hal.archives-ouvertes.fr/inria-00331193

. Sidi-ould and . Biha, Formalisation des mathématiques : une preuve du théorème de Cayley-Hamilton, Journées Francophones des Langages Applicatifs, pp.1-14, 2008.

J. Cowles, R. Gamboa, and J. Van-baalen, Using ACL2 Arrays to Formalize Matrix Algebra, ACL2 Workshop, 2003.

D. Delahaye and M. Mayero, Quantifier Elimination over Algebraically Closed Fields in a Proof Assistant using a Computer Algebra System, Proceedings of Calculemus 2005, pp.57-73, 2006.
DOI : 10.1016/j.entcs.2005.11.023

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

B. Duerte, Elements of Mathematical Analysis in PVS, Proceedings of the Ninth International Conference on Theorem Proving in Higher-Order Logics (TPHOL '96), 1996.

J. D. Fleuriot, On the Mechanization of Real Analysis in Isabelle/HOL
DOI : 10.1007/3-540-44659-1_10

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

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, TPHOLs, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11

URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier, Notation of the Four Colour Theorem proof

G. Gonthier and A. Mahboubi, A small scale reflection extension for the coq system
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 Euclidian Space, LNCS, vol.3603, pp.114-129, 2005.

J. Harrison and L. Théry, A Skeptic's Approach to Combining HOL and Maple, Journal of Automated Reasoning, vol.21, issue.3, pp.279-294, 1998.
DOI : 10.1023/A:1006023127567

N. Julien, Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base, Functional and Logic Programming Symposium (FLOPS), 2008.
DOI : 10.1007/978-3-540-78969-7_6

URL : https://hal.archives-ouvertes.fr/inria-00202744

N. Julien and I. Pasca, Formal Verification of Exact Computations Using Newton???s Method, TPHOLs, pp.408-423, 2009.
DOI : 10.1007/3-540-36126-X_17

R. David and . Lester, Real Number Calculations and Theorem Proving, Lecture Notes in Computer Science, vol.5170, pp.215-229, 2008.

N. Magaud, Ring properties for square matrices

M. Mayero, Formalisation et automatisation de preuves en analyses reelle et numerique, 2001.

S. Obua, Proving Bounds for Real Linear Programs in Isabelle/HOL, Theorem Proving in Higher-Order Logics, pp.227-244, 2005.
DOI : 10.1007/11541868_15

O. Russell and . Connor, Certified Exact Transcendental Real Number Computation in Coq, Theorem Proving in Higher Order Logics, 21st International Conference, pp.246-261, 2008.

I. Pa¸scapa¸sca, A Formal Verification for Kantorovitch's Theorem, Journées Francophones des Langages Applicatifs, pp.15-29, 2008.

J. Stein, Documentation for the formalization of Linerar Agebra

M. Analysis and .. , 13 2.3.2 Metric spaces: convergence, limit, continuity

C. Implementation-in and C. For, 28 3.3.1 Derivation, p.29