{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T17:47:38Z","timestamp":1773856058919,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_34","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T09:52:36Z","timestamp":1374486756000},"page":"463-468","source":"Crossref","is-referenced-by-count":27,"title":["The Picard Algorithm for Ordinary Differential Equations in Coq"],"prefix":"10.1007","author":[{"given":"Evgeny","family":"Makarov","sequence":"first","affiliation":[]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L. Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"key":"34_CR2","first-page":"1","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. MSCS, Special Issue on \u201cInteractive Theorem Proving and the Formalization of Mathematics\u201d\u00a021, 1\u201331 (2011)","journal-title":"MSCS, Special Issue on \u201cInteractive Theorem Proving and the Formalization of Mathematics\u201d"},{"key":"34_CR3","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. LMCS\u00a09(1:1) (2013), doi:10.2168\/LMCS-9(1:01)2013"},{"key":"34_CR4","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":"34_CR5","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: ICFP, pp. 163\u2013175 (2011)","DOI":"10.1145\/2034574.2034798"},{"key":"34_CR6","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. TCS\u00a0411, 3386\u20133402 (2010)","journal-title":"TCS"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Bridger, M.: Real analysis, a constructive approach. Pure and Applied Mathematics (New York). Wiley (2007)","DOI":"10.1002\/9781118033357"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-642-03359-9_28","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Julien","year":"2009","unstructured":"Julien, N., Pa\u015fca, I.: Formal Verification of Exact Computations Using Newton\u2019s Method. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 408\u2013423. Springer, Heidelberg (2009)"},{"issue":"15","key":"34_CR9","first-page":"1","volume":"4","author":"T. Coquand","year":"2012","unstructured":"Coquand, T., Spitters, B.: A constructive proof of Simpson\u2019s rule. Logic and Analysis\u00a04(15), 1\u20138 (2012)","journal-title":"Logic and Analysis"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-25379-9_26","volume-title":"Certified Programs and Proofs","author":"M. Boespflug","year":"2011","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 362\u2013377. Springer, Heidelberg (2011)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-32347-8_26","volume-title":"Interactive Theorem Proving","author":"F. Immler","year":"2012","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 377\u2013392. Springer, Heidelberg (2012)"},{"key":"34_CR12","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":"34_CR13","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. Journal of Automated Reasoning, 1\u201334 (2011)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,18]],"date-time":"2019-07-18T22:13:35Z","timestamp":1563488015000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}