{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:37Z","timestamp":1725663817187},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_149","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T08:26:55Z","timestamp":1330244815000},"page":"371-384","source":"Crossref","is-referenced-by-count":5,"title":["Modelling bit vectors in HOL: The word library"],"prefix":"10.1007","author":[{"given":"Wai","family":"Wong","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"29_CR1","unstructured":"R. J. Boulton. A HOL semantics for a subset of ELLA. Technical Report 254, University of Cambridge Computer Laboratory, 1992."},{"key":"29_CR2","unstructured":"A. J. Camilleri. Executing behavioural definitions in higher order logic. Technical Report 140, University of Cambridge Computer Laboratory, 1988."},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"A. Cohn. A proof of correctness of the VIPER microprocessor: the first level. Technical Report 104, University of Cambridge Computer Laboratory, January 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"29_CR4","unstructured":"A. Cohn. A proof of correctness of the VIPER microprocessor: the second level. Technical Report 134, University of Cambridge Computer Laboratory, May 1990."},{"key":"29_CR5","unstructured":"A. Cohn and M. J. C. Gordon. A machanized proof of correctness of a simple counter. Technical Report 94, University of Cambridge Computer Laborartory, July 1986."},{"key":"29_CR6","unstructured":"M. J. C. Gordon. Hardware verification by formal proof. Technical Report 74, University of Cambridge Computer Laborartory, 1985."},{"key":"29_CR7","unstructured":"Michael. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyan, editors, Formal Aspects of VLSI Design, pages 153\u2013178. Springer-Verlag, 1986."},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Brian T. Graham. The SECD Microprocessor \u2014 a Verification Case Study. Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3576-8"},{"key":"29_CR9","unstructured":"J. Joyce, G. Birtwistle, and M. J. C. Gordon. Proving a computer correct in higher order logic. Technical Report 100, University of Cambridge Computer Laborartory, December 1986."},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"J. J. Joyce. Formal specification and verification of microprocessor systems. In S. Winter and H. Schumny, editors, EUROMICRO 88:Proceedings of the 14th Symposium on Microprocessing and Microprogramming. Horth-Holland, 1988.","DOI":"10.1016\/0165-6074(88)90081-6"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"T. F. Melham. Automating recursive type definition in higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"29_CR12","unstructured":"T. F. Melham. Formalizing abstraction mechanisms for hardware verification in higher order logic. Technical Report 201, University of Cambridge Computer Laboratory, 1990."},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"T. F. Melham. The HOL logic extended with quantification over type variables. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications. Horth-Holland, 1993.","DOI":"10.1016\/B978-0-444-89880-7.50007-3"},{"key":"29_CR14","volume-title":"Technical Report 300","author":"W. Wong","year":"1993","unstructured":"W. Wong. Formal verification of VIPER's ALU. Technical Report 300, University of Cambridge Computer Laboratory, University of Cambridge Computer laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, ENGLAND, May 1993."},{"key":"29_CR15","unstructured":"W. Wong. The HOL res-quan Library. Computer Laboratory, University of Cambridge, 1993."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_149.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:30Z","timestamp":1605629670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_149"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_149","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}