J. Abdeljaoued and H. Lombardi, Méthodes matricielles -Introduction à la complexité algébrique, 2004.

H. Barendregt, H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, The " fundamental theorem of algebra " project

Y. Bertot, G. Gonthier, S. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

D. Coppersmith and S. Winograd, Matrix multiplication via arithmetic progressions, Proceedings of the nineteenth annual ACM conference on Theory of computing , STOC '87, pp.251-280, 1990.
DOI : 10.1145/28395.28396
URL : http://doi.org/10.1016/s0747-7171(08)80013-2

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

G. Gonthier, Formal proof?the four-color theorem, Notices of the, pp.1382-1393, 2008.

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, Interactive Theorem Proving, pp.103-118, 2011.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-00805966

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, LNCS, vol.4130, pp.423-437, 2006.
DOI : 10.1007/11814771_36

T. C. Hales, The jordan curve theorem, formally and informally, The American Mathematical Monthly, pp.882-894, 2007.

A. Karatsuba and Y. Ofman, Multiplication of many-digital numbers by automatic computers, In USSR Academy of Sciences, vol.145, pp.293-294, 1962.

D. E. Knuth, The art of computer programming, volume 2: seminumerical algorithms, 1981.

A. Mahboubi, Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials, 3rd International Joint Conference on Automated Reasoning (IJCAR), LNAI, pp.438-452, 2006.
DOI : 10.1007/11814771_37
URL : https://hal.archives-ouvertes.fr/inria-00001270

R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive Algebra, 1988.
DOI : 10.1007/978-1-4419-8640-5

R. O. Connor, Karatsuba's multiplication

R. O. Connor, Certified exact transcendental real number computation in coq, Theorem Proving in Higher Order Logics, pp.246-261, 2008.

F. Palomo-lozano, I. Medina-bulo, and J. Alonso-jiménez, Certification of matrix multiplication algorithms. strassen's algorithm in ACL2, Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, volume Informatics Research Report EDI-INF-RR-0046, 2001.

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

V. Strassen, Gaussian elimination is not optimal, Numerische Mathematik, vol.13, issue.4, pp.354-356, 1969.
DOI : 10.1007/BF02165411
URL : http://www.digizeitschriften.de/download/PPN362160546_0013/PPN362160546_0013___log38.pdf

S. Winograd, On multiplication of 2 ?? 2 matrices, Linear Algebra and its Applications, vol.4, issue.4, pp.381-388, 1971.
DOI : 10.1016/0024-3795(71)90009-7