Z. Ahmed, Ahmed's integral: the maiden solution, Mathematical Spectrum, vol.48, issue.1, pp.11-12, 2015.

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

J. W. Eaton, D. Bateman, S. Hauberg, and R. Wehbring, GNU Octave version 3.8.1 manual: a high-level interactive language for numerical computations, 2014.

J. Hass and R. Schlafly, Double Bubbles Minimize, The Annals of Mathematics, vol.151, issue.2, pp.459-515, 2000.
DOI : 10.2307/121042

H. A. Helfgott, Major arcs for Goldbach's problem, 1305.

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

E. Makarov, B. Spitters, ´. E. Martin-dorel, and G. Melquiond, The Picard algorithm for ordinary differential equations in Coq Proving tight bounds on univariate expressions with elementary functions in Coq, Interactive Theorem Proving (ITP), pp.463-468, 2013.

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

N. S. Nedialkov, Interval tools for ODEs and DAEs, Scientific Computing, 2006.

R. O. Connor and B. Spitters, A computer verified, monadic, functional implementation of the integral, Theoretical Computer Science, vol.411, issue.37, pp.3386-3402, 2010.

S. M. Rump, Verification methods, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC '10, pp.287-449, 2010.
DOI : 10.1145/1837934.1837937

W. Tucker, Validated Numerics: A Short Introduction to Rigorous Computations, 2011.