S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013.
DOI : 10.1007/s10817-012-9255-4

URL : https://hal.archives-ouvertes.fr/hal-00649240

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.1007/s11786-014-0181-1

URL : https://hal.archives-ouvertes.fr/hal-00860648

P. G. Ciarlet, The finite element method for elliptic problems, Classics in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM), vol.40, p.520174, 2002.

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

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

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14

URL : https://hal.archives-ouvertes.fr/hal-00816699

B. Gostiaux, Cours de mathématiques spéciales -Tome 2, Lecture notes in Special Mathematics -Tome 2]. Mathématiques [Mathematics] . Presses Universitaires de France, 1993.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in Isabelle, pp.279-294, 2013.

B. Huffman and O. Kun?ar, Lifting and Transfer: A Modular Design for Quotients in, pp.131-146978, 2013.

F. Immler, Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations, NASA Formal Methods -6th International Symposium, NFM 2014, pp.113-127, 2014.
DOI : 10.1007/978-3-319-06200-6_9

F. Immler and J. Hölzl, Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL, Interactive Theorem Proving -Third International Conference, ITP 2012, pp.377-392, 2012.
DOI : 10.1007/978-3-642-32347-8_26

F. Immler and C. Traut, The Flow of ODEs, Proceedings of the 7th International Conference on Interactive Theorem Proving, pp.184-199
DOI : 10.1007/978-3-319-03545-1_9

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.

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

. Mahboubi, The Rooster and the Butterflies URL https, CICM 2013 -Conference on Intelligent Computer Mathematics -2013, pp.1-18, 2013.

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, Interactive Theorem Proving -4th International Conference, pp.19-34978, 2013.
DOI : 10.1007/978-3-642-39634-2_5

URL : https://hal.archives-ouvertes.fr/hal-00816703

E. Makarov and B. Spitters, The Picard Algorithm for Ordinary Differential Equations in Coq, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.463-468, 2013.
DOI : 10.1007/978-3-642-39634-2_34

O. C. Zienkiewicz, R. L. Taylor, and J. Z. Zhu, The finite element method: its basis and fundamentals, 2013.