A HOL Theory of Euclidean Space, Theorem Proving in Higher Order Logics, pp.114-129, 2005. ,
DOI : 10.1007/11541868_8
Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904, 2009. ,
A brief overview of HOL, LNCS, vol.5170, pp.28-32, 2008. ,
A Theory of Matrices of Real Elements, Formalized Mathematics, vol.14, issue.1, pp.21-28, 2006. ,
DOI : 10.2478/v10037-006-0004-1
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
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
Formal Proofs for Theoretical Properties of Newton s Method. Rapport de recherché INRIA Sophia Antipolis, 28 pages, 2010. ,
Formally Verified Conditions for Regularity of Interval Matrices, Intelligent Computer Mathematics, p.2010 ,
URL : https://hal.archives-ouvertes.fr/inria-00464937
An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 1986. ,
DOI : 10.1007/978-94-015-9934-4
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
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
Representing a logic in the LCF metalanguage Tools and notions for program construction: an advanced course, pp.163-185, 1982. ,