{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T15:50:53Z","timestamp":1758124253678},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_12","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"147-162","source":"Crossref","is-referenced-by-count":18,"title":["Formal Proof of a Wave Equation Resolution Scheme: The Method Error"],"prefix":"10.1007","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Cl\u00e9ment","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Weis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Texts in Applied Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-7278-1","volume-title":"Numerical Partial Differential Equations: Finite Difference Methods","author":"J.W. Thomas","year":"1995","unstructured":"Thomas, J.W.: Numerical Partial Differential Equations: Finite Difference Methods. Texts in Applied Mathematics, vol.\u00a022. Springer, Heidelberg (1995)"},{"key":"12_CR2","volume-title":"Handbook of Differential Equations","author":"D. Zwillinger","year":"1998","unstructured":"Zwillinger, D.: Handbook of Differential Equations. Academic Press, London (1998)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/BFb0105402","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1996","unstructured":"Dutertre, B.: Elements of Mathematical Analysis in PVS. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 141\u2013156. Springer, Heidelberg (1996)"},{"key":"12_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-44659-1_10","volume-title":"Theorem Proving in Higher Order Logics","author":"J.D. Fleuriot","year":"2000","unstructured":"Fleuriot, J.D.: On the Mechanization of Real Analysis in Isabelle\/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 145\u2013161. Springer, Heidelberg (2000)"},{"key":"12_CR6","unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. PhD thesis, Universit\u00e9 Paris VI (2001)"},{"issue":"4","key":"12_CR7","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R. Gamboa","year":"2001","unstructured":"Gamboa, R., Kaufmann, M.: Nonstandard Analysis in ACL2. Journal of Automated Reasoning\u00a027(4), 323\u2013351 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-45842-5_6","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Niqui, M.: Constructive Reals in Coq: Axioms and Categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 79\u201395. Springer, Heidelberg (2002)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-39185-1_7","volume-title":"Types for Proofs and Programs","author":"L. Cruz-Filipe","year":"2003","unstructured":"Cruz-Filipe, L.: A Constructive Formalization of the Fundamental Theorem of Calculus. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 108\u2013126. Springer, Heidelberg (2003)"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-45685-6_17","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Mayero","year":"2002","unstructured":"Mayero, M.: Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 246\u2013262. Springer, Heidelberg (2002)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL Theory of Euclidean Space. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/s10817-007-9066-1","volume":"38","author":"J. Avigad","year":"2007","unstructured":"Avigad, J., Donnelly, K.: A Decision Procedure for Linear \u201dBig O\u201d Equations. J. Autom. Reason.\u00a038(4), 353\u2013373 (2007)","journal-title":"J. Autom. Reason."},{"key":"12_CR13","unstructured":"B\u00e9cache, E.: \u00c9tude de sch\u00e9mas num\u00e9riques pour la r\u00e9solution de l\u2019\u00e9quation des ondes. Master Mod\u00e9lisation et simulation, Cours ENSTA (2009), http:\/\/www-rocq.inria.fr\/~becache\/COURS-ONDES\/Poly-num-0209.pdf"},{"key":"12_CR14","volume-title":"Wave Propagation in Elastic Solids","author":"J.D. Achenbach","year":"1973","unstructured":"Achenbach, J.D.: Wave Propagation in Elastic Solids. North Holland, Amsterdam (1973)"},{"key":"12_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-85034-9","volume-title":"Mechanics of Continua and Wave Dynamics","author":"L.M. Brekhovskikh","year":"1994","unstructured":"Brekhovskikh, L.M., Goncharov, V.: Mechanics of Continua and Wave Dynamics. Springer, Heidelberg (1994)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Newton, I.: Axiomata, sive Leges Motus. In: Philosophiae Naturalis Principia Mathematica, London, vol.\u00a01 (1687)","DOI":"10.5479\/sil.52126.39088015628399"},{"key":"12_CR17","unstructured":"le Rond D\u2019Alembert, J.: Recherches sur la courbe que forme une corde tendue mise en vibrations. In: Histoire de l\u2019Acad\u00e9mie Royale des Sciences et Belles Lettres (Ann\u00e9e 1747), vol.\u00a03, pp. 214\u2013249. Haude et Spener, Berlin (1749)"},{"key":"12_CR18","volume-title":"Partial Differential Equations","author":"F. John","year":"1986","unstructured":"John, F.: Partial Differential Equations. Springer, Heidelberg (1986)"},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1147\/rd.112.0215","volume":"11","author":"R. Courant","year":"1967","unstructured":"Courant, R., Friedrichs, K., Lewy, H.: On the partial difference equations of mathematical physics. IBM Journal of Research and Development\u00a011(2), 215\u2013234 (1967)","journal-title":"IBM Journal of Research and Development"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-02930-1_8","volume-title":"Automata, Languages and Programming","author":"S. Boldo","year":"2009","unstructured":"Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol.\u00a05556, pp. 91\u2013102. Springer, Heidelberg (2009)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:59Z","timestamp":1606186019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}