J. D. Achenbach, Wave Propagation in Elastic Solids, Journal of Applied Mechanics, vol.41, issue.2, 1973.
DOI : 10.1115/1.3423344

J. Avigad and K. Donnelly, A Decision Procedure for Linear ???Big O??? Equations, Journal of Automated Reasoning, vol.5, issue.4:4, pp.353-373, 2007.
DOI : 10.1007/s10817-007-9066-1

´. E. Bécache, ´ Etude de schémas numériques pour la résolution de l'´ equation des ondes Master Modélisation et simulation, Cours ENSTA, 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, Floats and Ropes: A Case Study for Formal Numerical Program Verification, Proceedings of the 36th International Colloquium on Automata, Languages and Programming, pp.91-102, 2009.
DOI : 10.1007/978-3-642-02930-1_8

L. M. Brekhovskikh and V. Goncharov, Mechanics of Continua and Wave Dynamics, 1994.

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

L. Cruz-filipe, A Constructive Formalization of the Fundamental Theorem of Calculus, Proceedings of the 2nd International Workshop on Types for Proofs and Programs, 2002.
DOI : 10.1007/3-540-39185-1_7

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

J. D. Fleuriot, On the Mechanization of Real Analysis in Isabelle/HOL, 13th International Conference on Theorem Proving and Higher-Order Logic (TPHOLs'00), volume 1869 of LNCS, pp.145-161, 2000.
DOI : 10.1007/3-540-44659-1_10

R. Gamboa and M. Kaufmann, Nonstandard Analysis in ACL2, Journal of Automated Reasoning, vol.27, issue.4, pp.323-351, 2001.
DOI : 10.1023/A:1011908113514

H. Geuvers and M. Niqui, Constructive Reals in Coq: Axioms and Categoricity, Proceedings of the 1st International Workshop on Types for Proofs and Programs, pp.79-95, 2000.
DOI : 10.1007/3-540-45842-5_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.97.6910

J. Harrison, Theorem Proving with the Real Numbers, 1998.
DOI : 10.1007/978-1-4471-1591-5

F. John, Partial Differential Equations, 1986.

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.

P. Letouzey, A New Extraction for Coq, Proceedings of the 2nd International Workshop on Types for Proofs and Programs, 2002.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

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 Differentiation Algorithm) In Victor Carreño, César Muñoz, andSofì ene Tahar, 15th International Conference on Theorem Proving and Higher-Order Logic, pp.246-262, 2002.

I. Newton, Axiomata, sive Leges Motus, Philosophiae Naturalis Principia Mathematica, p.1687

D. Zwillinger, Handbook of Differential Equations, 1998.