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
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
The finite element method for elliptic problems, Classics in Applied Mathematics. Society for Industrial and Applied Mathematics (SIAM), vol.40, p.520174, 2002. ,
The Lax-Milgram Theorem. A detailed proof to be formalized in Coq URL https, 2016. ,
Theory and practice of finite elements, of Applied Mathematical Sciences, pp.978-979, 2004. ,
DOI : 10.1007/978-1-4757-4355-5
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
Cours de mathématiques spéciales -Tome 2, Lecture notes in Special Mathematics -Tome 2]. Mathématiques [Mathematics] . Presses Universitaires de France, 1993. ,
Type classes and filters for mathematical analysis in Isabelle, pp.279-294, 2013. ,
Lifting and Transfer: A Modular Design for Quotients in, pp.131-146978, 2013. ,
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
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
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
Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée, Thèse de doctorat, 2015. ,
How to express convergence for analysis in Coq, The 7th Coq Workshop, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01169321
The Rooster and the Butterflies URL https, CICM 2013 -Conference on Intelligent Computer Mathematics -2013, pp.1-18, 2013. ,
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
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
The finite element method: its basis and fundamentals, 2013. ,