{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:21Z","timestamp":1740123261825,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T00:00:00Z","timestamp":1694822400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T00:00:00Z","timestamp":1694822400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-20-CE48-0014"],"award-info":[{"award-number":["ANR-20-CE48-0014"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101001995"],"award-info":[{"award-number":["101001995"]}],"id":[{"id":"10.13039\/501100000781","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":[[2023,12]]},"DOI":"10.1007\/s10817-023-09679-x","type":"journal-article","created":{"date-parts":[[2023,9,16]],"date-time":"2023-09-16T04:01:32Z","timestamp":1694836892000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Enabling Floating-Point Arithmetic in the Coq Proof Assistant"],"prefix":"10.1007","volume":"67","author":[{"given":"\u00c9rik","family":"Martin-Dorel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Roux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,16]]},"reference":[{"key":"9679_CR1","doi-asserted-by":"publisher","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.) 1st International Conference on Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 6172, pp. 83\u201398. Edinburgh, UK (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_8","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"9679_CR2","doi-asserted-by":"publisher","unstructured":"Bertholon, G., Martin-Dorel, \u00c9., Roux, P.: Primitive floats in Coq. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving. Leibniz International Proceedings in Informatics, vol. 141, pp. 7\u20131720. Portland, OR, USA (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.7","DOI":"10.4230\/LIPIcs.ITP.2019.7"},{"key":"9679_CR3","doi-asserted-by":"publisher","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: 1st International Conference on Certified Programs and Proofs, Kenting, Taiwan, pp. 362\u2013377 (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_26","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"9679_CR4","doi-asserted-by":"publisher","unstructured":"Boldo, S., Jourdan, J.-H., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Nannarelli, A., Seidel, P.-M., Tang, P.T.P. (eds.) 21st IEEE Symposium on Computer Arithmetic, Austin, TX, USA, pp. 107\u2013115 (2013). https:\/\/doi.org\/10.1109\/ARITH.2013.30","DOI":"10.1109\/ARITH.2013.30"},{"key":"9679_CR5","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.) 20th IEEE Symposium on Computer Arithmetic, T\u00fcbingen, Germany, pp. 243\u2013252 (2011). https:\/\/doi.org\/10.1109\/ARITH.2011.40","DOI":"10.1109\/ARITH.2011.40"},{"key":"9679_CR6","unstructured":"Boldo, S., Munoz, C.: A high-level formalization of floating-point number in PVS. Technical Report 20070003560, NASA, National Institute of Aerospace, Hampton, VA, USA (2006)"},{"issue":"2","key":"9679_CR7","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10817-014-9317-x","volume":"54","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Jourdan, J.-H., Leroy, X., Melquiond, G.: Verified compilation of floating-point computations. J. Autom. Reason. 54(2), 135\u2013163 (2015). https:\/\/doi.org\/10.1007\/s10817-014-9317-x","journal-title":"J. Autom. Reason."},{"key":"9679_CR8","doi-asserted-by":"publisher","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) 3rd International Conference on Certified Programs and Proofs. Lecture Notes in Computer Science, vol. 8307, pp. 147\u2013162. Melbourne, Australia (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_10","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"9679_CR9","unstructured":"D\u00e9n\u00e8s, M.: Towards primitive data types for Coq 63-bits integers and persistent arrays. In: 5th Coq Workshop, Rennes, France (2013). https:\/\/coq.inria.fr\/files\/coq5_submission_2.pdf"},{"key":"9679_CR10","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: 7th ACM SIGPLAN International Conference on Functional Programming, Pittsburgh, PA, USA, pp. 235\u2013246 (2002). https:\/\/doi.org\/10.1145\/581478.581501","DOI":"10.1145\/581478.581501"},{"key":"9679_CR11","doi-asserted-by":"publisher","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.) 3rd International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 4130, pp. 423\u2013437. Seattle, WA, USA (2006). https:\/\/doi.org\/10.1007\/11814771_36","DOI":"10.1007\/11814771_36"},{"key":"9679_CR12","doi-asserted-by":"publisher","unstructured":"Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) 12th International Conference in Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1690, pp. 113\u2013130. Nice, France (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_9","DOI":"10.1007\/3-540-48256-3_9"},{"key":"9679_CR13","volume-title":"Accuracy and Stability of Numerical Algorithms","author":"N Higham","year":"1996","unstructured":"Higham, N.: Accuracy and Stability of Numerical Algorithms. Society for Industrial and Applied Mathematics, Philadelphia, PA (1996)"},{"key":"9679_CR14","doi-asserted-by":"publisher","unstructured":"IEEE Computer Society: IEEE standard for floating-point arithmetic. Technical Report 754-2008, IEEE (August 2008). https:\/\/doi.org\/10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"issue":"310","key":"9679_CR15","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1090\/mcom\/3234","volume":"87","author":"C Jeannerod","year":"2018","unstructured":"Jeannerod, C., Rump, S.M.: On relative errors of floating-point operations: optimal bounds and applications. Math. Comput. 87(310), 803\u2013819 (2018). https:\/\/doi.org\/10.1090\/mcom\/3234","journal-title":"Math. Comput."},{"key":"9679_CR16","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Bertot, Y., Vafeiadis, V. (eds.) 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Paris, France, pp. 90\u201399 (2017). https:\/\/doi.org\/10.1145\/3018610.3018622","DOI":"10.1145\/3018610.3018622"},{"issue":"3","key":"9679_CR17","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10817-015-9350-4","volume":"57","author":"\u00c9 Martin-Dorel","year":"2016","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 57(3), 187\u2013217 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9350-4","journal-title":"J. Autom. Reason."},{"key":"9679_CR18","unstructured":"Miner, P.: Defining the IEEE-854 floating-point standard in PVS. Technical Report 19950023402, NASA, Langley Research Center, Hampton, VA, USA (1995)"},{"issue":"3","key":"9679_CR19","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30(3), 12\u201311241 (2008). https:\/\/doi.org\/10.1145\/1353445.1353446","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9679_CR20","volume-title":"Interval Analysis","author":"RE Moore","year":"1963","unstructured":"Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs, NJ (1963)"},{"key":"9679_CR21","doi-asserted-by":"publisher","unstructured":"Muller, J.-M., Brunie, N., Dinechin, F., Jeannerod, C.-P., Joldes, M., Lef\u00e8vre, V., Melquiond, G., Revol, N., Torres, S.: Handbook of Floating-Point Arithmetic, 2nd edn. Birkh\u00e4user, Basel (2018). https:\/\/doi.org\/10.1007\/978-3-319-76526-6","DOI":"10.1007\/978-3-319-76526-6"},{"issue":"2","key":"9679_CR22","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10817-015-9339-z","volume":"57","author":"P Roux","year":"2016","unstructured":"Roux, P.: Formal proofs of rounding error bounds\u2014with application to an automatic positive definiteness check. J. Autom. Reason. 57(2), 135\u2013156 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9339-z","journal-title":"J. Autom. Reason."},{"key":"9679_CR23","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10543-006-0056-1","volume":"46","author":"SM Rump","year":"2006","unstructured":"Rump, S.M.: Verification of positive definiteness. BIT Numer. Math. 46, 433\u2013452 (2006)","journal-title":"BIT Numer. Math."},{"key":"9679_CR24","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S096249291000005X","volume":"19","author":"SM Rump","year":"2010","unstructured":"Rump, S.M.: Verification methods: rigorous results using floating-point arithmetic. Acta Numer. 19, 287\u2013449 (2010). https:\/\/doi.org\/10.1017\/S096249291000005X","journal-title":"Acta Numer."},{"key":"9679_CR25","unstructured":"Spiwack, A.: Verified computing in homological algebra. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (2011). https:\/\/tel.archives-ouvertes.fr\/pastel-00605836"},{"key":"9679_CR26","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s002080010018","volume":"2","author":"W Tucker","year":"2002","unstructured":"Tucker, W.: A rigorous ODE solver and Smale\u2019s 14th problem. Found. Comput. Math. 2, 53\u2013117 (2002). https:\/\/doi.org\/10.1007\/s002080010018","journal-title":"Found. Comput. Math."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09679-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09679-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09679-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,9]],"date-time":"2023-12-09T09:04:42Z","timestamp":1702112682000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09679-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,16]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["9679"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09679-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,9,16]]},"assertion":[{"value":"8 June 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 August 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 September 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interest"}}],"article-number":"33"}}