{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:40:54Z","timestamp":1773654054998,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540678632","type":"print"},{"value":"9783540446590","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_15","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"233-251","source":"Crossref","is-referenced-by-count":33,"title":["Formal Verification of IA-64 Division Algorithms"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Marius Cornea, Cristina Iordache, Peter Markstein, and John Harrison. Integer divide and remainder operations in the Intel IA-64 architecture. In Jean-Claude Ba-jard, Christiane Frougny, Peter Kornerup, and Jean-Michel Muller, editors, RNC4, the fourth international conference on Real Numbers and Computers, pages 161\u2013184, 2000."},{"key":"15_CR2","first-page":"1","volume":"1998-Q2","author":"M. Cornea-Hasegan","year":"1998","unstructured":"Marius Cornea-Hasegan. Proving the IEEE correctness of iterative floating-point square root, divide and remainder algorithms. Intel Technology Journal, 1998-Q2:1\u201311, 1998. See http:\/\/developer.intel.com\/technology\/itj\/q21998\/articles\/art_3.htm .","journal-title":"Intel Technology Journal"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Guy Cousineau and Michel Mauny. The Functional Approach to Programming. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"issue":"7","key":"15_CR4","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/2.689674","volume":"64","author":"C. Dulong","year":"1998","unstructured":"Carole Dulong. The IA-64 architecture at work. IEEE Computer, 64(7):24\u201332, July 1998.","journal-title":"IEEE Computer"},{"key":"15_CR5","unstructured":"Michael J. C. Gordon and Thomas F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. J. C. Gordon","year":"1979","unstructured":"Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"FMCAD\u201996","author":"J. Harrison","year":"1996","unstructured":"John Harrison. HOL Light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, FMCAD\u201996, volume 1166 of Lecture Notes in Computer Science, pages 265\u2013269. Springer-Verlag, 1996."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"John Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author\u2019s PhD thesis.","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"TPHOLs\u201999","author":"J. Harrison","year":"1999","unstructured":"John Harrison. A machine-checked theory of floating point arithmetic. In Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin, and Laurent Th\u00e9ry, editors, TPHOLs\u201999, volume 1690 of Lecture Notes in Computer Science, pages 113\u2013130, 1999. Springer-Verlag."},{"key":"15_CR10","unstructured":"IEEE. Standard for binary floating point arithmetic. ANSI\/IEEE Standard 754-1985, The Institute of Electrical and Electronic Engineers, Inc."},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1147\/rd.341.0111","volume":"34","author":"P. Markstein","year":"1990","unstructured":"Peter Markstein. Computation of elementary functions on the IBM RISC System\/6000 processor. IBM Journal of Research and Development, 34:111\u2013119, 1990.","journal-title":"IBM Journal of Research and Development"},{"key":"15_CR12","unstructured":"Peter Markstein. IA-64 and Elementary Functions: Speed and Precision. Prentice-Hall, 2000."},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J. S. Moore","year":"1998","unstructured":"J Strother Moore, Tom Lynch, and Matt Kaufmann. A mechanically checked proof of the correctness of the kernel of the AM D5k86 floating-point division program. IEEE Transactions on Computers, 47:913\u2013926, 1998.","journal-title":"IEEE Transactions on Computers"},{"key":"15_CR14","first-page":"1","volume":"1999-Q1","author":"J. O\u2019Leary","year":"1999","unstructured":"John O\u2019Leary, Xudong Zhao, Rob Gerth, and Carl-Johan H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, 1999-Q1:1\u201314, 1999. http:\/\/developer.intel.com\/technology\/itj\/ql1999\/articles\/art_5.htm .","journal-title":"Intel Technology Journal"},{"key":"15_CR15","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"David Rusinoff. A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics, 1:148\u2013200, 1998. Available on the Web via http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html .","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"15_CR16","unstructured":"Pierre Weis and Xavier Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http:\/\/pauillac.inria.fr\/caml\/ ."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:32:58Z","timestamp":1556695978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}