{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:44Z","timestamp":1725663824821},"publisher-location":"Berlin, Heidelberg","reference-count":13,"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_128","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T08:27:21Z","timestamp":1330244841000},"page":"101-114","source":"Crossref","is-referenced-by-count":0,"title":["A functional approach for formalizing regular hardware structures"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Eisenbiegler","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"8_CR1","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Herbert, and J. van Tassel. Experiences with Embedding hardware description languages in HOL. In V. Stavridou, T.F. Melham, and R. Boute, editors, Conference on Theorem Provers in Circuit Design, IFIP Transactions A-10, pages 129\u2013156. North-Holland, 1992."},{"key":"8_CR2","unstructured":"R. Boulton, M. Gordon, J. Herbert, and J. van Tassel. The HOL verification of ELLA designs. In International Workshop on Formal Methods in VLSI Design, January 1991."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"D. Borrione, L. Pierre, and A. Salem. Formal verification of VHDL descriptions in Boyer-Moore: First results. In J. Mermet, editor, VDHL for Simulation, Synthesis and Formal Proofs of Hardware, pages 227\u2013243. Kluwer Academic Press, 1992.","DOI":"10.1007\/978-1-4615-3562-1_16"},{"key":"8_CR4","unstructured":"A. Camilleri, M.J.C. Gordon, and Th. Melham. Hardware verification using higher order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 41\u201366. North-Holland, 1986."},{"key":"8_CR5","unstructured":"J. Camilleri. Executing behavioural definitions in higher order logic. Technical Report 140, University of Cambridge Computer Laboratory, 1988."},{"key":"8_CR6","unstructured":"J. Camilleri. Symbolic compilation and execution of programs by proof: a case study in HOL. Technical Report 240, University of Cambridge Computer Laboratory, 1991."},{"key":"8_CR7","first-page":"561","volume-title":"Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions","author":"E. Gunter","year":"1992","unstructured":"E. Gunter. Why we can't have SML-style datatype declarations in HOL. In L.J.M. Claesen and M.J.C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions, pages 561\u2013568, Leuven, Belgium, 1992. North-Holland."},{"key":"8_CR8","unstructured":"W.A. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89\u2013132. North-Holland, 1986."},{"key":"8_CR9","unstructured":"S.L.P. Jones. The Implementation of Functional Programming Languages. Prentice Hall, 1987."},{"issue":"2","key":"8_CR10","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"R. Kumar, K. Schneider, and Th. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. Journal of Formal Methods in System Design, 2(2):165\u2013223, 1993.","journal-title":"Journal of Formal Methods in System Design"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"T. F. Melham. Automating recursive type definitions in higher order logic. Technical Report 146, University of Cambridge Computer Laboratory, September 1988.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"K. Schneider, R. Kumar, and Th. Kropf. Eliminating higher-order quanitifers to obtain decision procedures for hardware verification. In International Workshop on Higher-Order Logic Theorem Proving and its Applications, Vancouver, Canada, August 1993.","DOI":"10.1007\/3-540-57826-9_150"},{"key":"8_CR13","first-page":"289","volume-title":"The fusion of Hardware Design and Verification","author":"M. Sheeran","year":"1988","unstructured":"M. Sheeran. Retiming and slowdown in Ruby. In G.J. Milne, editor, The fusion of Hardware Design and Verification, pages 289\u2013308, Glasgow, 1988. North Holland."}],"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_128.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:25Z","timestamp":1605629665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_128","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}