{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T16:27:07Z","timestamp":1780936027735,"version":"3.54.1"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,10,5]],"date-time":"2015-10-05T00:00:00Z","timestamp":1444003200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche (FR)","doi-asserted-by":"publisher","award":["ID0EANAE45"],"award-info":[{"award-number":["ID0EANAE45"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10817-015-9350-4","type":"journal-article","created":{"date-parts":[[2015,10,5]],"date-time":"2015-10-05T06:33:48Z","timestamp":1444026828000},"page":"187-217","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq"],"prefix":"10.1007","volume":"57","author":[{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,10,5]]},"reference":[{"issue":"3","key":"9350_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010). doi: 10.1007\/s10817-009-9149-2","journal-title":"J. Autom. Reason."},{"key":"9350_CR2","doi-asserted-by":"publisher","unstructured":"Allamigeon, X., Gaubert, S., Magron, V., Werner, B.: Certification of bounds of non-linear functions: the templates method. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics\u2014MKM, Calculemus, DML, and Systems and Projects. Lecture Notes in Computer Science, vol. 7961, pp. 51\u201365 (2013). doi: 10.1007\/978-3-642-39320-4_4","DOI":"10.1007\/978-3-642-39320-4_4"},{"key":"9350_CR3","doi-asserted-by":"publisher","unstructured":"Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pp. 243\u2013252. T\u00fcbingen, Germany (2011). doi: 10.1109\/ARITH.2011.40","DOI":"10.1109\/ARITH.2011.40"},{"key":"9350_CR4","doi-asserted-by":"publisher","unstructured":"Brisebarre, N., Jolde\u015f, M., Martin-Dorel, \u00c9., Mayero, M., Muller, J.M., Pa\u015fca, I., Rideau, L., Th\u00e9ry, L.: Rigorous polynomial approximation using Taylor models in Coq. In: Goodloe, A., Person, S. (eds.) Proceedings of 4th International Symposium on NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 85\u201399. Springer, Norfolk (2012). doi: 10.1007\/978-3-642-28891-3_9","DOI":"10.1007\/978-3-642-28891-3_9"},{"issue":"1","key":"9350_CR5","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s00607-002-1448-y","volume":"69","author":"M Ceberio","year":"2002","unstructured":"Ceberio, M., Granvilliers, L.: Horner\u2019s rule for interval evaluation revisited. Computing 69(1), 51\u201381 (2002). doi: 10.1007\/s00607-002-1448-y","journal-title":"Computing"},{"issue":"16","key":"9350_CR6","doi-asserted-by":"publisher","first-page":"1523","DOI":"10.1016\/j.tcs.2010.11.052","volume":"412","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. J. Theor. Comput. Sci. 412(16), 1523\u20131543 (2011). doi: 10.1016\/j.tcs.2010.11.052","journal-title":"J. Theor. Comput. Sci."},{"key":"9350_CR7","doi-asserted-by":"crossref","unstructured":"Chevillard, S., Jolde\u015f, M., Lauter, C.: Sollya: an environment for the development of numerical codes. In: Fukuda, K., van\u00a0der Hoeven, J., Joswig, M., Takayama, N. (eds.) Proceedings of the 3rd International Congress on Mathematical Software, Lecture Notes in Computer Science, vol. 6327, pp. 28\u201331. Heidelberg (2010)","DOI":"10.1007\/978-3-642-15582-6_5"},{"issue":"2","key":"9350_CR8","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: a library for interval arithmetic. IEEE Trans. Comput. 58(2), 226\u2013237 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"9350_CR9","doi-asserted-by":"publisher","unstructured":"Daumas, M., Melquiond, G., Mu\u00f1oz, C.: Guaranteed proofs using interval arithmetic. In: Montuschi, P., Schwarz, E. (eds.) Proceedings of the 17th IEEE Symposium on Computer Arithmetic, pp. 188\u2013195. Cape Cod, MA (2005). doi: 10.1109\/ARITH.2005.25","DOI":"10.1109\/ARITH.2005.25"},{"key":"9350_CR10","doi-asserted-by":"publisher","unstructured":"Denman, W., Mu\u00f1oz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM, Lecture Notes in Computer Science, vol. 8442, pp. 194\u2013199. Springer (2014). doi: 10.1007\/978-3-319-06410-9_14","DOI":"10.1007\/978-3-319-06410-9_14"},{"key":"9350_CR11","doi-asserted-by":"crossref","DOI":"10.1201\/9780203026922","volume-title":"Global Optimization Using Interval Analysis: Revised and Expanded. Monographs and Textbooks in Pure and Applied Mathematics","author":"E Hansen","year":"2003","unstructured":"Hansen, E., Walster, G.: Global Optimization Using Interval Analysis: Revised and Expanded. Monographs and Textbooks in Pure and Applied Mathematics. CRC Press, Boca Raton (2003)"},{"key":"9350_CR12","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Verifying the accuracy of polynomial approximations in HOL. In: Gunter, E.L., Felty, A.P. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1275, pp. 137\u2013152. Murray Hill, NJ, USA (1997). doi: 10.1007\/BFb0028391","DOI":"10.1007\/BFb0028391"},{"key":"9350_CR13","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 4732, pp. 102\u2013118. Kaiserslautern, Germany (2007)","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"9350_CR14","unstructured":"Jolde\u015f, M.: Rigorous Polynomial Approximations and Applications. Ph.D. thesis, ENS de Lyon, France (2011). http:\/\/tel.archives-ouvertes.fr\/tel-00657843\/en\/"},{"key":"9350_CR15","unstructured":"Makino, K.: Rigorous Analysis of Nonlinear Motion in Particle Accelerators. Ph.D. thesis, Michigan State University, East Lansing, Michigan, USA (1998)"},{"issue":"4","key":"9350_CR16","first-page":"379","volume":"4","author":"K Makino","year":"2003","unstructured":"Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math. 4(4), 379\u2013456 (2003)","journal-title":"Int. J. Pure Appl. Math."},{"key":"9350_CR17","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Mayero, M., Pa\u015fca, I., Rideau, L., Th\u00e9ry, L.: Certified, efficient and sharp univariate Taylor models in Coq. In: IEEE, SYNASC 2013, pp. 193\u2013200. Timi\u015foara, Romania (2013). doi: 10.1109\/SYNASC.2013.33","DOI":"10.1109\/SYNASC.2013.33"},{"key":"9350_CR18","unstructured":"Melquiond, G.: Floating-point arithmetic in the Coq system. In: Proceedings of the 8th Conference on Real Numbers and Computers, pp. 93\u2013102. Santiago de Compostela, Spain (2008)"},{"key":"9350_CR19","doi-asserted-by":"publisher","unstructured":"Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 5195, pp. 2\u201317. Sydney, Australia (2008). doi: 10.1007\/978-3-540-71070-7_2","DOI":"10.1007\/978-3-540-71070-7_2"},{"key":"9350_CR20","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.ic.2011.09.005","volume":"216","author":"G Melquiond","year":"2012","unstructured":"Melquiond, G.: Floating-point arithmetic in the Coq system. Inf. Comput. 216, 14\u201323 (2012). doi: 10.1016\/j.ic.2011.09.005","journal-title":"Inf. Comput."},{"key":"9350_CR21","volume-title":"Interval Analysis","author":"RE Moore","year":"1966","unstructured":"Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)"},{"key":"9350_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"JM Muller","year":"2010","unstructured":"Muller, J.M., Brisebarre, N., de Dinechin, F., Jeannerod, C.P., Lef\u00e8vre, V., Melquiond, G., Revol, N., Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user, Boston (2010). doi: 10.1007\/978-0-8176-4705-6"},{"issue":"2","key":"9350_CR23","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151\u2013196 (2013). doi: 10.1007\/s10817-012-9256-3","journal-title":"J. Autom. Reason."},{"key":"9350_CR24","doi-asserted-by":"publisher","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) Proceedings of the 5th International Conference on Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, vol. 8164, pp. 326\u2013343. Menlo Park, CA, USA (2013). doi: 10.1007\/978-3-642-54108-7_17","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"9350_CR25","doi-asserted-by":"publisher","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) Proceedings of the 5th International Symposium on NASA Formal Methods. Lecture Notes in Computer Science, vol. 7871, pp. 383\u2013397. Moffett Field, CA, USA (2013). doi: 10.1007\/978-3-642-38088-4_26","DOI":"10.1007\/978-3-642-38088-4_26"},{"issue":"2","key":"9350_CR26","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/63522.214389","volume":"15","author":"PTP Tang","year":"1989","unstructured":"Tang, P.T.P.: Table-driven implementation of the exponential function in IEEE floating-point arithmetic. ACM Trans. Math. Softw. 15(2), 144\u2013157 (1989). doi: 10.1145\/63522.214389","journal-title":"ACM Trans. Math. Softw."},{"issue":"3","key":"9350_CR27","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. Softw. 17(3), 410\u2013423 (1991). doi: 10.1145\/114697.116813","journal-title":"ACM Trans. Math. Softw."},{"key":"9350_CR28","unstructured":"Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, \u00c9cole polytechnique, France (2008). http:\/\/alacave.net\/~roland\/FormalGlobalOpt.pdf"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9350-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9350-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9350-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,22]],"date-time":"2022-05-22T17:16:09Z","timestamp":1653239769000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9350-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,5]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["9350"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9350-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,10,5]]}}}