. Coq, Art : The Calculus of Inductive Constructions, Texts in Theoretical Computer Science

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, Proceedings of the 1st International Conference on Interactive Theorem Proving, p.147162, 2010.
DOI : 10.1007/978-3-642-14052-5_12

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

S. Boutin, Using reection to build ecient and certied decision procedures, Proceedings of the 3th International Symposium on Theoretical Aspects of Computer Software TACS'97, p.515529, 1997.

D. Delahaye, A Tactic Language for the System Coq, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning, p.377440, 2000.
DOI : 10.1007/3-540-44404-1_7

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

B. Dutertre, Elements of mathematical analysis in PVS, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics TPHOL, pp.141-156, 1996.
DOI : 10.1007/BFb0105402

J. D. Fleuriot, On the Mechanization of Real Analysis in Isabelle/HOL, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.145161, 2000.
DOI : 10.1007/3-540-44659-1_10

G. Gonthier, Formal proof the four-color theorem. Notices of the AMS, p.13821393, 2008.

J. Harrison, Constructing the real numbers in HOL. Formal Methods in System Design, p.3559, 1994.

J. Le-rond and D. , Recherches sur la courbe que forme une corde tendue mise en vibrations

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

M. Mayero, Using theorem proving for numerical analysis (correctness proof of an automatic dierentiation algorithm) In Victor Carreño, César Muñoz, and Soène Tahar, Proceedings of the 15th International Conference on Theorem Proving and Higher-Order Logic, p.246262, 2002.

G. Melquiond, Proving Bounds on Real-Valued Functions with Computations
DOI : 10.1007/978-3-540-71070-7_2

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

E. W. Weisstein, D'Alembert's Solution. From MathWorldA Wolfram Web Resource http