F. Barbanera and S. Berardi, Abstract, Journal of Functional Programming, vol.6, issue.03, pp.519-525, 1996.
DOI : 10.1016/0890-5401(88)90005-3

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

. 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.

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher-Order Logics, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

J. Harrison, . Hol, and . Light, A Tutorial Introduction, FMCAD, pp.265-269, 1996.

J. Harrison, A HOL Theory of Euclidian Space, LNCS, vol.3603, pp.114-129, 2005.

G. Huet and A. Sa¨?bisa¨?bi, Constructive category theory, Proof, language , and interaction: essays in honour of Robin Milner, pp.239-275, 2000.

F. Kammuller, Modular Structures as Dependent Types in Isabelle, Proc. TYPES Workshop, pp.121-132, 1998.
DOI : 10.1007/3-540-48167-2_9

N. Magaud, Ring properties for square matrices

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

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

C. Lawrence and . Paulson, Organizing Numerical Theories Using Axiomatic Type Classes, J. Autom. Reason, vol.33, issue.1, pp.29-49, 2004.

R. Pollack, Dependently Typed Records for Representing Mathematical Structure, TPHOLs '00: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, pp.462-479, 2000.
DOI : 10.1007/3-540-44659-1_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.9569

J. Stein, Documentation for the formalization of Linerar Agebra