{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:15Z","timestamp":1776423795873,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642323461","type":"print"},{"value":"9783642323478","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_26","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T07:33:54Z","timestamp":1344584034000},"page":"377-392","source":"Crossref","is-referenced-by-count":34,"title":["Numerical Analysis of Ordinary Differential Equations in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Fabian","family":"Immler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14052-5_12","volume-title":"Interactive Theorem Proving","author":"S. Boldo","year":"2010","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Formal Proof of a Wave Equation Resolution Scheme: The Method Error. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 147\u2013162. Springer, Heidelberg (2010)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Bornemann, V., Deuflhard, P.: Scientific computing with ordinary differential equations (2002)","DOI":"10.1007\/978-0-387-21582-2"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code Generation via Higher-Order Rewrite Systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2009","unstructured":"Haftmann, F., Wenzel, M.: Local Theory Specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"key":"26_CR5","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Ph.D. thesis (1996)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"26_CR7","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Reis, G.D., Th\u00e9ry, L. (eds.) Programming Languages for Mechanized Mathematics Systems (ACM SIGSAM PLMMS 2009), pp. 38\u201345 (2009)"},{"key":"26_CR8","unstructured":"Immler, F., H\u00f6lzl, J.: Ordinary Differential Equations. Archive of Formal Proofs (April 2012), \n                    \n                      http:\/\/afp.sf.net\/entries\/Ordinary_Differential_Equations.shtml\n                    \n                    \n                  , Formal proof development"},{"key":"26_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-22673-1_7","volume-title":"Intelligent Computer Mathematics","author":"R. Krebbers","year":"2011","unstructured":"Krebbers, R., Spitters, B.: Computer Certified Efficient Exact Reals in COQ. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS (LNAI), vol.\u00a06824, pp. 90\u2013106. Springer, Heidelberg (2011)"},{"key":"26_CR10","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in COQ. CoRR abs\/1106.3448 (2011)"},{"key":"26_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-71070-7_2","volume-title":"Automated Reasoning","author":"G. Melquiond","year":"2008","unstructured":"Melquiond, G.: Proving Bounds on Real-Valued Functions with Computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 2\u201317. Springer, Heidelberg (2008)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/11541868_13","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Mu\u00f1oz","year":"2005","unstructured":"Mu\u00f1oz, C., Lester, D.R.: Real Number Calculations and Theorem Proving. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 195\u2013210. Springer, Heidelberg (2005)"},{"key":"26_CR13","unstructured":"Obua, S.: Flyspeck II: The Basic Linear Programs. Ph.D. thesis, M\u00fcnchen (2008)"},{"issue":"37","key":"26_CR14","doi-asserted-by":"publisher","first-page":"3386","DOI":"10.1016\/j.tcs.2010.05.031","volume":"411","author":"R. O\u2019Connor","year":"2010","unstructured":"O\u2019Connor, R., Spitters, B.: A computer verified, monadic, functional implementation of the integral. Theoretical Computer Science\u00a0411(37), 3386\u20133402 (2010)","journal-title":"Theoretical Computer Science"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified Exact Transcendental Real Number Computation in COQ. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 246\u2013261. Springer, Heidelberg (2008)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Reinhardt, H.J.: Numerik gew\u00f6hnlicher Differentialgleichungen. de Gruyter (2008)","DOI":"10.1515\/9783110206791"},{"key":"26_CR17","unstructured":"Spitters, B.: Numerical integration in COQ, Mathematics, Algorithms, and Proofs (MAP 2010) (November 2010), \n                    \n                      www.unirioja.es\/dptos\/dmc\/MAP2010\/Slides\/Slides\/talkSpittersMAP2010.pdf"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Walter, W.: Ordinary Differential Equations, 1st edn. Springer (1998)","DOI":"10.1007\/978-1-4612-0601-9_1"}],"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-32347-8_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T08:01:09Z","timestamp":1620115269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}