{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:07Z","timestamp":1767927907617,"version":"3.49.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,7]]},"DOI":"10.1109\/arith.2011.40","type":"proceedings-article","created":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T16:03:27Z","timestamp":1314288207000},"page":"243-252","source":"Crossref","is-referenced-by-count":94,"title":["Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq"],"prefix":"10.1109","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"217","article-title":"Formal verification of floating-point trigonometric functions","author":"hunt","year":"0","journal-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design"},{"key":"ref11","first-page":"169","article-title":"A generic library of floating-point numbers and its application to exact computing","author":"daumas","year":"0","journal-title":"Proc 10th Int Conf Theorem Proving Higher Order Logics"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_6"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2003.1207663"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1023\/B:NUMA.0000049487.98618.61","article-title":"A simple test qualifying the accuracy of Horner's rule for polynomials","volume":"37","year":"2004","journal-title":"Numerical Algorithms"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_2"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1236463.1236468"},{"key":"ref4","article-title":"Formalisation en Coq de la norme IEEE-754 sur I'arithmétiquc à virgule flottante","author":"loiseleur","year":"1997"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"ref3","article-title":"Specification of the IEEE-854 floating-point standard in HOL and PVS","author":"carre\u00f1o","year":"0","journal-title":"Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its Applications"},{"key":"ref6","first-page":"3","article-title":"A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon processor","volume":"1954","author":"russinoff","year":"0","journal-title":"Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/12.713311"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1613-y"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0081-6"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/32.24710"},{"key":"ref9","first-page":"113","article-title":"A machine-checked theory of floating point arithmetic","author":"harrison","year":"0","journal-title":"Proceedings of the 12th International Conference on Theorem Proving in Higher"},{"key":"ref1","first-page":"754","article-title":"IEEE Computer Society","year":"2008","journal-title":"IEEE Standard for Floating-Point Arithmetic"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.1991.145549"},{"key":"ref22","author":"sterbenz","year":"1974","journal-title":"Floating-Point Computation"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022973506233"},{"key":"ref24","volume":"2","author":"knuth","year":"1998","journal-title":"The art of computer programming"},{"key":"ref23","author":"higham","year":"1996","journal-title":"Accuracy and Stability of Numerical Algorithms"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2007.20"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1137\/030601818"}],"event":{"name":"2011 IEEE 20th Symposium on Computer Arithmetic (ARITH)","location":"Tuebingen, Germany","start":{"date-parts":[[2011,7,25]]},"end":{"date-parts":[[2011,7,27]]}},"container-title":["2011 IEEE 20th Symposium on Computer Arithmetic"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx5\/5991607\/5992089\/05992132.pdf?arnumber=5992132","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T05:10:39Z","timestamp":1497935439000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/ieeexplore.ieee.org\/document\/5992132\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":27,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/arith.2011.40","relation":{},"subject":[],"published":{"date-parts":[[2011,7]]}}}