{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:12:51Z","timestamp":1781892771264,"version":"3.54.5"},"reference-count":26,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput."],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1109\/tc.2008.216","type":"journal-article","created":{"date-parts":[[2008,12,18]],"date-time":"2008-12-18T16:15:00Z","timestamp":1229616900000},"page":"1139-1145","source":"Crossref","is-referenced-by-count":10,"title":["Formally Verified Argument Reduction with a Fused Multiply-Add"],"prefix":"10.1109","volume":"58","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"Daumas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ren-Cang","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","article-title":"A Machine-Checked Theory of Floating Point Arithmetic","author":"harrison","year":"1999","journal-title":"Proc 12th Int'l Conf Theorem Proving in Higher Order Logics (TPHOLs '99)"},{"key":"ref11","first-page":"217","article-title":"Formal Verification of Floating Point Trigonometric Functions","author":"harrison","year":"2000","journal-title":"Proc Third Int'l Conf Formal Methods in Computer-Aided Design (FMCAD '00)"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","article-title":"A Generic Library of Floating-Point Numbers and Its Application to Exact Computing","author":"daumas","year":"2001","journal-title":"Proc 14th Int'l Conf Theorem Proving in Higher Order Logics (TPHOLs '01)"},{"key":"ref13","author":"bertot","year":"2004","journal-title":"Texts in Theoretical Computer Science"},{"key":"ref14","article-title":"Specification of the IEEE-854 Floating-Point Standard in HOL and PVS","author":"carre\ufffdo","year":"1995","journal-title":"Proc 1995 Int'l Workshop Higher Order Logic Theorem Proving and Its Applications"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1112\/S1461157000000176"},{"key":"ref16","author":"harrison","year":"1997","journal-title":"Floating-Point Verification in HOL Light The Exponential Function"},{"key":"ref17","author":"sterbenz","year":"1974","journal-title":"Floating Point Computation"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0120-y"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.15"},{"key":"ref3","author":"muller","year":"2006","journal-title":"Elementary Functions Algorithms and Implementation"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1147\/rd.341.0111"},{"key":"ref5","author":"cody","year":"1980","journal-title":"Software Manual for the Elementary Functions"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2003.1207670"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.1999.762822"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2005.36"},{"key":"ref9","author":"kahan","year":"1983","journal-title":"Minimizing q x m ? n"},{"key":"ref1","author":"markstein","year":"2000","journal-title":"IA-64 and Elementary Functions Speed and Precision"},{"key":"ref20","first-page":"9","article-title":"An American National Standard: IEEE Standard for Binary Floating Point Arithmetic","volume":"22","author":"stevenson","year":"1987","journal-title":"ACM SIGPLAN Notices"},{"key":"ref22","year":"1996","journal-title":"Pentium Pro Family Developer's Manual Programmer's Reference Manual"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/MM.1984.291224"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2005.39"},{"key":"ref23","year":"0"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(75)90022-8"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/279232.279237"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/12\/5165572\/04711042.pdf?arnumber=4711042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,29]],"date-time":"2021-11-29T20:40:57Z","timestamp":1638218457000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/4711042\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":26,"journal-issue":{"issue":"8"},"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/tc.2008.216","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}