{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:09:13Z","timestamp":1761610153529,"version":"build-2065373602"},"reference-count":21,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3893,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s1571-0661(04)80408-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"132-144","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"title":["Properties of the subtraction valid for any floating point system"],"prefix":"10.1016","volume":"66","author":[{"given":"Sylvie","family":"Boldo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Daumas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB1","unstructured":"Amerkad A., Y. Bertot, L. Rideau and L. Pottier, Mathematics and proof presentation in Pcoq, in: Proceedings of Proof Transformation and Presentation and Proof Complexities, Siena, Italy, 2001. URL http:\/\/www-sop.inria.fr\/lemme\/Laurence.Rideau\/proof-pco\\%q.ps.gz."},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB2","unstructured":"Carre\u00f1o, V. A. and P. S. Miner, Specification of the IEEE-854 floatingpoint standard in HOL and PVS, in: 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, 1995, supplemental Proceedings. URL http:\/\/shemesh.larc.nasa.gov\/fm\/ftp\/larc\/vac\/hug95.ps"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB3","unstructured":"Coonen, J. T., Specification for a proposed standard for floating point arithmetic, Memorandum ERL M78\/72, University of California, Berkeley (1978)."},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Cowlishaw, M. F., E. M. Schwarz, R. M. Smith and C. F. Webb, A decimal floating point specification, in: N. Burgess and L. Ciminiera, editors, Proceedings of the 15th Symposium on Computer Arithmetic, Vail, Colorado, 2001, pp. 147\u2013154. URL http:\/\/computer.org\/proceedings\/arith\/","DOI":"10.1109\/ARITH.2001.930114"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB5","article-title":"Additive symmetric: the non-negative case","author":"Daumas","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Daumas M., L. Rideau and L. Th\u00e9ry, A generic library of floating-point numbers and its application to exact computing, in: 14th International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, 2001, pp. 169\u2013184. URL http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/2\\%152\/21520169.htm.","DOI":"10.1007\/3-540-44755-5_13"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB7","doi-asserted-by":"crossref","first-page":"887","DOI":"10.1137\/0905062","article-title":"Underflow and the reliability of numerical software","volume":"5","author":"Demmel","year":"1984","journal-title":"SIAM Journal on Scientific and Statistical Computing"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Goldberg D., What every computer scientist should know about floating point arithmetic, ACM Computing Surveys 23 (1991), pp. 5\u201347. URL http:\/\/www.acm.org\/pubs\/articles\/journals\/surveys\/1991-\\%23-1\/p5-goldberg.pdf","DOI":"10.1145\/103162.103163"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Harrison J., Floating point verification in HOL light: the exponential function, Technical Report 428, University of Cambridge Computer Laboratory (1997). URL http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/tang.ps.gz","DOI":"10.1007\/BFb0000475"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB10","unstructured":"Higham, N. J., \u201cAccuracy and stability of numerical algorithms,\u201d SIAM, 1996. URL http:\/\/www.ma.man.ac.uk\/~higham\/asna.html"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB11","unstructured":"Huet G., G. Kahn and C. Paulin-Mohring, The Coq proof assistant: a tutorial: version 6.1, Technical Report 204, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France (1997). URL ftp:\/\/ftp.inria.fr\/INRIA\/publication\/publi-pdf\/RT\/RT-02\\%04.pdf"},{"year":"1997","series-title":"\u201cThe Art of Computer Programming: Seminumerical Algorithms\u201d","author":"Knuth","key":"10.1016\/S1571-0661(04)80408-0_NEWBIB12"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB13","unstructured":"Kulisch U., Rounding near zero, in: 4th Real Numbers and Computers Conference, Dagstuhl, Germany, 2000, pp. 23\u201329."},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Laurent O., P. Michel and V. Wiels, Using formal verification techniques to reduce simulation and test effort, in: International Symposium of Formal Methods Europe, Berlin, Germany, 2001, pp. 465\u2013477. URL http:\/\/link.springer.de\/link\/service\/series\/0558\/papers\\%\/2021\/20210465.pdf","DOI":"10.1007\/3-540-45251-6_27"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB15","doi-asserted-by":"crossref","unstructured":"Overton, M. J., \u201cNumerical Computing with IEEE Floating Point Arithmetic,\u201d SIAM, 2001. URL http:\/\/www.siam.org\/catalog\/mcc07\/ot76.htm","DOI":"10.1137\/1.9780898718072"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB16","doi-asserted-by":"crossref","unstructured":"Rushby J. and F. von Henke, Formal verification of algorithms for critical systems, in: Proceedings of the Conference on Software for Critical Systems, New Orleans, Louisiana, 1991, pp. 1\u201315. URL http:\/\/www.acm.org\/pubs\/articles\/proceedings\/soft\/12508\\%3\/p1-rushby\/p1-rushby.pdf.","DOI":"10.1145\/125083.123044"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB17","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","article-title":"A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor","volume":"1","author":"Russinoff","year":"1998","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB18","unstructured":"Schryer, N. L., A test of computer's floating-point arithmetic unit, Technical report 89, AT&T Bell Laboratories (1981). URL http:\/\/cm.bell-labs.com\/cm\/cs\/cstr\/89.ps.gz"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB19","doi-asserted-by":"crossref","unstructured":"Schwarz, E. M., R. M. Smith and C. A. Krygowski, The S\/390 G5 floating point unit supporting hex and binary architectures, in: I. Koren and P. Kornerup, editors, Proceedings of the 14th Symposium on Computer Arithmetic, Adelaide, Australia, 1999, pp. 258\u2013265. URL http:\/\/computer.org\/proceedings\/arith\/0116\/0116toc.htm","DOI":"10.1109\/ARITH.1999.762852"},{"year":"1974","series-title":"\u201cFloating point computation\u201d","author":"Sterbenz","key":"10.1016\/S1571-0661(04)80408-0_NEWBIB20"},{"key":"10.1016\/S1571-0661(04)80408-0_NEWBIB21","unstructured":"Texas Instruments, \u201cTMS320C3x \u2014 User's guide,\u201d (1997). URL http:\/\/www-s.ti.com\/sc\/psheets\/spru031e\/spru031e.pdf"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804080?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804080?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:04:34Z","timestamp":1761609874000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804080"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S1571066104804080"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80408-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Properties of the subtraction valid for any floating point system","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80408-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}