S. K. Afshar, V. Aravantinos, O. Hasan, and S. Tahar, Formalization of complex vectors in higher-order logic. CoRR, abs/1405, 2014.

J. Alberty, C. Carstensen, S. Funken, and R. Klose, Matlab implementation of the finite element method in elasticity, Computing, vol.69, issue.3, pp.239-263, 2002.
DOI : 10.1007/s00607-002-1459-8

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq Formal Proof of the Lax?Milgram theorem, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.79-89, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01391578

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

N. Bourbaki, Topologie générale: Chapitres 1 ` a 4, 1971.

F. Clément and V. Martin, The Lax-Milgram Theorem. A detailed proof to be formalized in Coq, 2016.

J. and D. Mallagaray, Formalisation and execution of Linear Algebra: theorems and algorithms, 2016.

A. Ern and J. L. Guermond, Theory and practice of finite elements, Applied Mathematical Sciences, vol.159, 2004.
DOI : 10.1007/978-1-4757-4355-5

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, pp.333-333, 2008.
DOI : 10.1007/978-3-540-87827-8_28

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving -4th International Conference Proceedings, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

B. Gostiaux, Topologie, analyse réelle. [15] J. Harrison. A HOL theory of Euclidean space, Cours de mathématiques spéciales -Tome 2. Mathématiques. Presses Universitaires de France Theorem Proving in Higher Order Logics, 18th International Conference, 1993.

J. Harrison, HOL Light: An Overview, Theorem Proving in Higher Order Logics, 22nd International Conference Proceedings, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in Isabelle/HOL, Interactive Theorem Proving -4th International Conference, ITP 2013 Proceedings, pp.279-294, 2013.

P. Howard and J. E. Rubin, Consequences of the Axiom of Choice. Number v. 1, 1998.

D. E. Knuth, The Art of Computer Programming): Seminumerical Algorithms, 1997.

C. Lelay, How to express convergence for analysis in Coq, The 7th Coq Workshop, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01169321

C. Lelay, Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée, Thèse de doctorat, 2015.

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, Interactive Theorem Proving -4th International Conference, ITP 2013 Proceedings, pp.19-34, 2013.
DOI : 10.1007/978-3-642-39634-2_5
URL : https://hal.archives-ouvertes.fr/hal-00816703

M. Y. Mahmoud, V. Aravantinos, and S. Tahar, Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory, NASA Formal Methods, 5th International Symposium, NFM 2013. Proceedings, pp.413-427, 2013.
DOI : 10.1007/978-3-642-38088-4_28

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, Automated Deduction -CADE-11, 11th International Conference on Automated Deduction Proceedings, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.49, issue.3, pp.363-397, 1989.
DOI : 10.1007/BF00248324

C. J. Purcell, Building finite element models with mathematica, Mathematica Developer Conference, 1997.

B. Spitters, Constructive and intuitionistic integration theory and function al analysis, 2002.