{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:41:44Z","timestamp":1754484104977},"publisher-location":"Berlin, Heidelberg","reference-count":7,"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_151","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:27:01Z","timestamp":1330262821000},"page":"399-412","source":"Crossref","is-referenced-by-count":3,"title":["Toward a super duper hardware tactic"],"prefix":"10.1007","author":[{"given":"Mark D.","family":"Aagaard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miriam E.","family":"Leeser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phillip J.","family":"Windley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"M. D. Aagaard and M. E. Leeser. A methodology for reusable hardware proofs. In L. Claesen and M. Gordon, editors, HOL Theorem Proving System and its Applications. North-Holland, September 1992.","DOI":"10.1016\/B978-0-444-89880-7.50018-8"},{"key":"31_CR2","unstructured":"A. Camillieri, M. Gordon, and T. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. North Holland, September 1986."},{"issue":"9","key":"31_CR3","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/32.58783","volume":"16","author":"F. K. Hanna","year":"1990","unstructured":"F. K. Hanna, N. Daeche, and M. Longley. Specification and verification using dependent types. IEEE Trans. on Soft. Eng., 16(9):949\u2013964, September 1990.","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In M. Archer and M. Gordon, editors, The HOL Theorem Proving System and its Applications, pages 170\u2013176. IEEE Press, 1991.","DOI":"10.1109\/HOL.1991.596284"},{"key":"31_CR5","unstructured":"M. E. Leeser. Using Nuprl for the verification and synthesis of hardware. In C. A. R. Hoare and M. J. C. Gordon, editors, Mechanized Reasoning and Hardware Design. Prentice-Hall International Series on Computer Science, 1992."},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"J. O'Leary et al. HML: a hardware description language based on SML. In D. Agnew and L. Claesen, editors, CHDL, Apr. 1993.","DOI":"10.1016\/B978-0-444-81641-2.50029-0"},{"key":"31_CR7","unstructured":"K. Schneider, R. Kumar, and T. Kropf. Structuring hardware proofs: First steps toward automation a higher order environment. In VLSI, 1991."}],"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_151.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:46:24Z","timestamp":1640929584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_151"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_151","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}