G. E. Andrews, R. Askey, and R. Roy, Special functions, 1999.

R. Askey and G. Gasper, Certain Rational Functions Whose Power Series Have Positive Coefficients, The American Mathematical Monthly, vol.79, issue.4, pp.327-341, 1972.
DOI : 10.2307/2978081

P. Baudin, P. Cuoq, J. Filliâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language, version 1, 2009.

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

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pasca, Canonical Big Operators, 21st International Conference on 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

S. Boldo, Preuves formelles en arithmétiquesarithmétiquesà virgule flottante, 2004.

S. Boldo, Floats and Ropes: A Case Study for Formal Numerical Program Verification, 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009.
DOI : 10.1007/978-3-642-02930-1_8

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Formal Proof of a Wave Equation Resolution Scheme: The Method Error, 1st Conference on Interactive Theorem Proving Conference, pp.147-162, 2010.
DOI : 10.1007/978-3-642-14052-5_12

URL : https://hal.archives-ouvertes.fr/inria-00450789

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Annotated source code and Coq proofs, 2012.

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 and J. Filliâtre, Formal Verification of Floating-Point Programs, 18th IEEE Symposium on Computer Arithmetic (ARITH '07), pp.187-194, 2007.
DOI : 10.1109/ARITH.2007.20

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

S. Boldo, J. Filliâtre, and G. Melquiond, Combining Coq and Gappa for Certifying Floating-Point Programs, 16th Calculemus Symposium, pp.59-74, 2009.
DOI : 10.1109/TC.2008.200

URL : https://hal.archives-ouvertes.fr/inria-00432726

S. Boldo, J. Jourdan, X. Leroy, and G. Melquiond, A formallyverified C compiler supporting floating-point arithmetic, Proceedings of the 21th IEEE Symposium on Computer Arithmetic, pp.107-115, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00743090

S. Boldo, C. Lelay, and G. Melquiond, Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Proceedings of the Second International Conference on Certified Programs and Proofs, number 7679 in LNCS, pp.289-304, 2012.
DOI : 10.1007/978-3-642-35308-6_22

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

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40

URL : https://hal.archives-ouvertes.fr/inria-00534854

E. Sylvain-conchon, J. Contejean, S. Kanig, and . Lescuyer, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, Post-proceedings of the 5th International Workshop on Satisfiability Modulo Theories, pp.51-69, 2007.
DOI : 10.1016/j.entcs.2008.04.080

T. Coquand and C. Paulin-mohring, Inductively defined types, Colog'88, 1990.
DOI : 10.1007/3-540-52335-9_47

R. Courant, K. Friedrichs, and H. Lewy, On the Partial Difference Equations of Mathematical Physics, IBM Journal of Research and Development, vol.11, issue.2, pp.215-234, 1967.
DOI : 10.1147/rd.112.0215

M. Daumas and G. Melquiond, Certification of bounds on expressions involving rounded operators, ACM Transactions on Mathematical Software, vol.37, issue.1, pp.1-20, 2010.
DOI : 10.1145/1644001.1644003

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

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Proceedings of the 14th International Conference on Theorem Proving in Higher-Order Logics (TPHOL'01), pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13

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

C. Florent-de-dinechin, G. Lauter, and . Melquiond, Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, vol.60, issue.2, pp.242-253, 2011.
DOI : 10.1109/TC.2010.128

L. De, M. , and N. Bjørner, Z3, an efficient SMT solver, Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), pp.337-340, 2008.

W. Edsger and . Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.

A. Ern and M. Vohralík, Adaptive Inexact Newton Methods with A Posteriori Stopping Criteria for Nonlinear Diffusion PDEs, SIAM Journal on Scientific Computing, vol.35, issue.4, pp.1761-1791, 2014.
DOI : 10.1137/120896918

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

L. Fejér, Sur le développement d'une fonction arbitraire suivant les fonctions de Laplace. Comptes-Rendus de l'Académie des Sciences, pp.224-227, 1908.

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, 19th International Conference on Computer Aided Verification, pp.173-177, 2007.
DOI : 10.1007/978-3-540-73368-3_21

G. Gasper, Positive Sums of the Classical Orthogonal Polynomials, SIAM Journal on Mathematical Analysis, vol.8, issue.3, pp.423-447, 1977.
DOI : 10.1137/0508032

D. Goldberg, What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol.23, issue.1, pp.5-48, 1991.
DOI : 10.1145/103162.103163

F. John, Partial Differential Equations, 1986.

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

J. Le-rond and D. , Recherches sur la courbe que forme une corde tendue mise en vibrations, Histoire de l'Académie Royale des Sciences et Belles Lettres, pp.214-249, 1747.

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814

URL : https://hal.archives-ouvertes.fr/inria-00415861

C. Marché, Jessie, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.1-2, 2007.
DOI : 10.1145/1292597.1292598

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

L. William, C. J. Oberkampf, and . Roy, Verification and Validation in Scientific Computing, 2010.

C. John and . Strikwerda, Finite Difference Schemes and Partial Differential Equations, 1989.