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

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.

F. Faissole, Formalization and closedness of finite dimensional subspaces, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01630411

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

J. Harrison, A HOL Theory of Euclidean Space, Theorem Proving in Higher Order Logics, 18th International Conference, 2005.
DOI : 10.1007/11541868_8

A. Mahboubi, The Rooster and the Butterflies, CICM 2013 -Conference on Intelligent Computer Mathematics - 2013, pp.1-18, 2013.
DOI : 10.1007/978-3-642-39320-4_1
URL : https://hal.archives-ouvertes.fr/hal-00825074

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