{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:14:13Z","timestamp":1763468053031},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_9","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"85-99","source":"Crossref","is-referenced-by-count":9,"title":["Rigorous Polynomial Approximation Using Taylor Models in Coq"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Brisebarre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mioara","family":"Jolde\u015f","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micaela","family":"Mayero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Michel","family":"Muller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ioana","family":"Pa\u015fca","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Abramowitz, M., Stegun, I.A.: Handbook of mathematical functions with formulas, graphs, and mathematical tables. National Bureau of Standards Applied Mathematics Series, vol.\u00a055. For sale by the Superintendent of Documents, U.S. Government Printing Office, Washington, D.C (1964)","key":"9_CR1"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"M. Armand","year":"2010","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 83\u201398. Springer, Heidelberg (2010)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-15582-6_7","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"A. Benoit","year":"2010","unstructured":"Benoit, A., Chyzak, F., Darrasse, A., Gerhold, S., Mezzarobba, M., Salvy, B.: The Dynamic Dictionary of Mathematical Functions (DDMF). In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol.\u00a06327, pp. 35\u201341. Springer, Heidelberg (2010)"},{"key":"9_CR4","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","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)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1577190.1577198","volume-title":"SNC 2009: Proceedings of the 2009 Conference on Symbolic Numeric Computation","author":"M. Berz","year":"2009","unstructured":"Berz, M., Makino, K.: Rigorous global search using Taylor models. In: SNC 2009: Proceedings of the 2009 Conference on Symbolic Numeric Computation, pp. 11\u201320. ACM, New York (2009)"},{"doi-asserted-by":"crossref","unstructured":"Berz, M., Makino, K., Kim, Y.K.: Long-term stability of the tevatron by verified global optimization. Nuclear Instruments and Methods in Physics Research Section A: Accelerators, Spectrometers, Detectors and Associated Equipment\u00a0558(1), 1\u201310 (2006);","key":"#cr-split#-9_CR6.1","DOI":"10.1016\/j.nima.2005.11.035"},{"unstructured":"Proceedings of the 8th International Computational Accelerator Physics Conference - ICAP 2004","key":"#cr-split#-9_CR6.2"},{"key":"9_CR7","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)"},{"doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. In: Proceedings of the 20th IEEE Symposium on Computer Arithmetic, T\u00fcbingen, Germany, pp. 243\u2013252 (2011)","key":"9_CR8","DOI":"10.1109\/ARITH.2011.40"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1109\/ARITH.2007.17","volume-title":"18th IEEE Symposium on Computer Arithmetic","author":"N. Brisebarre","year":"2007","unstructured":"Brisebarre, N., Chevillard, S.: Efficient polynomial L\n                \u2009\u221e\u2009-approximations. In: Kornerup, P., Muller, J.M. (eds.) 18th IEEE Symposium on Computer Arithmetic, pp. 169\u2013176. IEEE Computer Society, Los Alamitos (2007)"},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/1141885.1141890","volume":"32","author":"N. Brisebarre","year":"2006","unstructured":"Brisebarre, N., Muller, J.M., Tisserand, A.: Computing Machine-efficient Polynomial Approximations. ACM Trans. Math. Software\u00a032(2), 236\u2013256 (2006)","journal-title":"ACM Trans. Math. Software"},{"unstructured":"Ch\u00e1ves, F.: Utilisation et certification de l\u2019arithm\u00e9tique d\u2019intervalles dans un assistant de preuves. Th\u00e8se, \u00c9cole normale sup\u00e9rieure de Lyon - ENS LYON (September 2007), \n                  \n                    http:\/\/tel.archives-ouvertes.fr\/tel-00177109\/en\/","key":"9_CR11"},{"unstructured":"Chevillard, S.: \u00c9valuation efficace de fonctions num\u00e9riques. Outils et exemples. Ph.D. thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon, Lyon, France (2009), \n                  \n                    http:\/\/tel.archives-ouvertes.fr\/tel-00460776\/fr\/","key":"9_CR12"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-15582-6_5","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"S. Chevillard","year":"2010","unstructured":"Chevillard, S., Jolde\u015f, M., Lauter, C.: Sollya: An Environment for the Development of Numerical Codes. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol.\u00a06327, pp. 28\u201331. Springer, Heidelberg (2010)"},{"issue":"412","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1523","DOI":"10.1016\/j.tcs.2010.11.052","volume":"16","author":"S. Chevillard","year":"2011","unstructured":"Chevillard, S., Harrison, J., Jolde\u015f, M., Lauter, C.: Efficient and accurate computation of upper bounds of approximation errors. Theoretical Computer Science\u00a016(412), 1523\u20131543 (2011)","journal-title":"Theoretical Computer Science"},{"unstructured":"Collins, P., Niqui, M., Revol, N.: A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq. In: NSV-3: Third International Workshop on Numerical Software Verification (2010)","key":"9_CR15"},{"doi-asserted-by":"crossref","unstructured":"de Dinechin, F., Lauter, C., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: Proceedings of the 2006 ACM Symposium on Applied Computing, Dijon, France, pp. 1318\u20131322 (2006), \n                  \n                    http:\/\/www.lri.fr\/~melquion\/doc\/06-mcms-article.pdf","key":"9_CR16","DOI":"10.1145\/1141277.1141584"},{"key":"9_CR17","volume-title":"Modern computer algebra","author":"J. Gathen von zur","year":"2003","unstructured":"von zur Gathen, J., Gerhard, J.: Modern computer algebra, 2nd edn. Cambridge University Press, New York (2003)","edition":"2"},{"key":"9_CR18","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)"},{"unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)","key":"9_CR19"},{"key":"9_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11814771_36","volume-title":"Automated Reasoning","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L.: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 423\u2013437. Springer, Heidelberg (2006)"},{"unstructured":"Griewank, A.: Evaluating Derivatives - Principles and Techniques of Algorithmic Differentiation. SIAM (2000)","key":"9_CR21"},{"unstructured":"IEEE Computer Society: IEEE Standard for Floating-Point Arithmetic. IEEE Std 754TM-2008 (August 2008)","key":"9_CR22"},{"unstructured":"Jolde\u015f, M.: Rigourous Polynomial Approximations and Applications. Ph.D. dissertation, \u00c9cole Normale Sup\u00e9rieure de Lyon, Lyon, France (2011), \n                  \n                    http:\/\/perso.ens-lyon.fr\/mioara.joldes\/these\/theseJoldes.pdf","key":"9_CR23"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","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.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 90\u2013106. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Lef\u00e8vre, V., Muller, J.M.: Worst cases for correct rounding of the elementary functions in double precision. In: Burgess, N., Ciminiera, L. (eds.) Proceedings of the 15th IEEE Symposium on Computer Arithmetic (ARITH-16), Vail, CO (June 2001)","key":"9_CR25","DOI":"10.1109\/ARITH.2001.930110"},{"unstructured":"Lizia, P.D.: Robust Space Trajectory and Space System Design using Differential Algebra. Ph.D. thesis, Politecnico di Milano, Milano, Italy (2008)","key":"9_CR26"},{"unstructured":"Makino, K.: Rigorous Analysis of Nonlinear Motion in Particle Accelerators. Ph.D. thesis, Michigan State University, East Lansing, Michigan, USA (1998)","key":"9_CR27"},{"issue":"4","key":"9_CR28","first-page":"379","volume":"4","author":"K. Makino","year":"2003","unstructured":"Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. International Journal of Pure and Applied Mathematics\u00a04(4), 379\u2013456 (2003), \n                  \n                    http:\/\/bt.pa.msu.edu\/pub\/papers\/TMIJPAM03\/TMIJPAM03.pdf","journal-title":"International Journal of Pure and Applied Mathematics"},{"unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. Ph.D. thesis, Universit\u00e9 Paris VI (2001)","key":"9_CR29"},{"key":"9_CR30","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)"},{"doi-asserted-by":"crossref","unstructured":"Moore, R.E.: Methods and Applications of Interval Analysis. Society for Industrial and Applied Mathematics (1979)","key":"9_CR31","DOI":"10.1137\/1.9781611970906"},{"unstructured":"Muller, J.M.: Projet ANR TaMaDi \u2013 Dilemme du fabricant de tables \u2013 Table Maker\u2019s Dilemma (ref. ANR 2010 BLAN 0203 01), \n                  \n                    http:\/\/tamadiwiki.ens-lyon.fr\/tamadiwiki\/","key":"9_CR32"},{"key":"9_CR33","volume-title":"Elementary Functions, Algorithms and Implementation","author":"J.M. Muller","year":"2006","unstructured":"Muller, J.M.: Elementary Functions, Algorithms and Implementation, 2nd edn. Birkh\u00e4user, Boston (2006)","edition":"2"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1137\/050638448","volume":"45","author":"M. Neher","year":"2007","unstructured":"Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM J. Numer. Anal.\u00a045, 236\u2013262 (2007)","journal-title":"SIAM J. Numer. Anal."},{"issue":"1","key":"9_CR35","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1023\/A:1023061927787","volume":"9","author":"A. Neumaier","year":"2003","unstructured":"Neumaier, A.: Taylor forms \u2013 use and limits. Reliable Computing\u00a09(1), 43\u201379 (2003)","journal-title":"Reliable Computing"},{"key":"9_CR36","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)"},{"unstructured":"The Ar\u00e9naire Project: CRlibm, Correctly Rounded mathematical library (July 2006), \n                  \n                    http:\/\/lipforge.ens-lyon.fr\/www\/crlibm\/","key":"9_CR37"},{"key":"9_CR38","first-page":"2063","volume":"198","author":"E. Remez","year":"1934","unstructured":"Remez, E.: Sur un proc\u00e9d\u00e9 convergent d\u2019approximations successives pour d\u00e9terminer les polyn\u00f4mes d\u2019approximation. C.R. Acad\u00e9mie des Sciences\u00a0198, 2063\u20132065 (1934) (in French)","journal-title":"C.R. Acad\u00e9mie des Sciences"},{"issue":"2","key":"9_CR39","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/178365.178368","volume":"20","author":"B. Salvy","year":"1994","unstructured":"Salvy, B., Zimmermann, P.: Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable. ACM Trans. Math. Software\u00a020(2), 163\u2013177 (1994)","journal-title":"ACM Trans. Math. Software"},{"issue":"2","key":"9_CR40","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0195-6698(80)80051-5","volume":"1","author":"R.P. Stanley","year":"1980","unstructured":"Stanley, R.P.: Differentiably finite power series. European Journal of Combinatorics\u00a01(2), 175\u2013188 (1980)","journal-title":"European Journal of Combinatorics"},{"issue":"3","key":"9_CR41","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/114697.116813","volume":"17","author":"A. Ziv","year":"1991","unstructured":"Ziv, A.: Fast evaluation of elementary mathematical functions with correctly rounded last bit. ACM Trans. Math. Software\u00a017(3), 410\u2013423 (1991)","journal-title":"ACM Trans. Math. Software"},{"key":"9_CR42","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11814771_35","volume-title":"Automated Reasoning","author":"R. Zumkeller","year":"2006","unstructured":"Zumkeller, R.: Formal Global Optimisation with Taylor Models. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 408\u2013422. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:27Z","timestamp":1620126867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}