J. Harrison, A HOL Theory of Euclidean Space, Theorem Proving in Higher Order Logics, pp.114-129, 2005.
DOI : 10.1007/11541868_8

C. , R. M. Solovay, R. D. Arthan, and J. Harrison, Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904, 2009.

K. Slind and M. Norrish, A brief overview of HOL, LNCS, vol.5170, pp.28-32, 2008.

Y. Nakamura, N. Tamura, and W. Chang, A Theory of Matrices of Real Elements, Formalized Mathematics, vol.14, issue.1, pp.21-28, 2006.
DOI : 10.2478/v10037-006-0004-1

N. Tamura and Y. Nakamura, Determinant and Inverse of Matrices of Real Elements, Formalized Mathematics, vol.15, issue.3, pp.127-136, 2007.
DOI : 10.2478/v10037-007-0014-7

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

I. Pasca, Formal Proofs for Theoretical Properties of Newton s Method. Rapport de recherché INRIA Sophia Antipolis, 28 pages, 2010.

I. Pasca, Formally Verified Conditions for Regularity of Interval Matrices, Intelligent Computer Mathematics, p.2010
URL : https://hal.archives-ouvertes.fr/inria-00464937

P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 1986.
DOI : 10.1007/978-94-015-9934-4

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society, vol.51, issue.1, pp.176-178, 1975.
DOI : 10.1090/S0002-9939-1975-0373893-X

M. J. Gordon, Representing a logic in the LCF metalanguage Tools and notions for program construction: an advanced course, pp.163-185, 1982.