{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T20:10:46Z","timestamp":1736021446536,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_5","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"20-34","source":"Crossref","is-referenced-by-count":6,"title":["Formalization of the DE2 Language"],"prefix":"10.1007","author":[{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"first","affiliation":[]},{"given":"Erik","family":"Reeber","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1145\/289423.289440","volume-title":"The International Conference on Functional Programming (ICFP)","author":"P. Bjesse","year":"1998","unstructured":"Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware Design in Haskell. In: The International Conference on Functional Programming (ICFP), vol.\u00a032(1), pp. 174\u2013184. ACM Press, New York (1998)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-30494-4_2","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2004","unstructured":"Sheeran, M.: Generating Fast Multipliers Using Clever Circuits. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 6\u201320. Springer, Heidelberg (2004)"},{"key":"5_CR3","first-page":"32","volume-title":"Principles and Practice of Declarative Programming (PPDP)","author":"S. Krstic","year":"2004","unstructured":"Krstic, S., Matthews, J.: Semantics of the reFLect Language. In: Principles and Practice of Declarative Programming (PPDP), pp. 32\u201342. ACM Press, New York (2004)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M.D. Aagaard","year":"1999","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, p. 323. Springer, Heidelberg (1999)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-40922-X_17","volume-title":"Formal Methods in Computer-Aided Design","author":"M.D. Aagaard","year":"2000","unstructured":"Aagaard, M.D., Jones, R.B., O\u2019Leary, J.W., Seger, C.-J.H., Melham, T.F.: A methodology for large-scale hardware verification. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 263\u2013282. Springer, Heidelberg (2000)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Sethumadhavan, S., Desikan, R., Burger, D., Moore, C.R., Keckler, S.W.: Scalable Hardware Memory Disambiguation for High ILP Processors (Load\/Store Queue Design). In: 36th International Symposium on Microarchitecture (MICRO 36), pp. 399\u2013410 (2003)","DOI":"10.1109\/MICRO.2003.1253244"},{"key":"5_CR7","unstructured":"The Tera-op Reliable Intelligently adaptive Processing System(TRIPS), http:\/\/www.cs.utexas.edu\/users\/cart\/trips\/"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.: ACL2 Theorems about Commercial Microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Sawada, J.: Formal Verification of an Advanced Pipelined Machine. PhD Thesis, University of Texas at Austin (1999)","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"5_CR10","first-page":"151","volume-title":"Computer-aided Reasoning: ACL2 case studies","author":"W.A. Hunt Jr.","year":"2000","unstructured":"Hunt Jr., W.A.: The DE Language. In: Computer-aided Reasoning: ACL2 case studies, pp. 151\u2013166. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"5_CR11","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, Boston (1988)"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","key":"5_CR12","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"5_CR13","first-page":"129","volume-title":"Theorem Provers in Circuit Design","author":"R. Boulton","year":"1992","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Theorem Provers in Circuit Design, IFIP Transactions A-10, pp. 129\u2013156. Elsevier Science Publishers, Amsterdam (1992)"},{"key":"5_CR14","unstructured":"Gordon, M.: Why Higher-order Logic is a Good Formalism for Specifying and Verifying Hardware. Technical Report\u00a077, University of Cambridge, Computer Laboratory (1985)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Hunt Jr., W.A., Brock, B.C.: A Formal HDL and Its Use in the FM9001 Verification. In: Hoare, C.A.R., Gordon, M.J.C. (eds.) Mechanized Reasoning and Hardware Design. Prentice-Hall International Series in Computer Science, pp. 35\u201348 (1992)","DOI":"10.1098\/rsta.1992.0024"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/CMPASS.1996.507872","volume-title":"Eleventh Annual Conference on Computer Assurance (COMPASS 1996)","author":"M. Kaufmann","year":"1996","unstructured":"Kaufmann, M., Moore, J.S.: ACL2: An Industrial Strength Version of NQTHM. In: Eleventh Annual Conference on Computer Assurance (COMPASS 1996), pp. 23\u201334. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"5_CR17","unstructured":"Steele, G.: Common Lisp: The Lanugage, 2nd edn. Digital Press (1990)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/3-540-59047-1_41","volume-title":"Theorem Provers in Circuit Design. Theory, Practice and Experience","author":"P.J. Windley","year":"1995","unstructured":"Windley, P.J., Coe, M.L.: A Correctness Model for Pipelined Microprocessors. In: Kumar, R., Kropf, T. (eds.) TPCD 1994. LNCS, vol.\u00a0901, pp. 33\u201351. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T19:51:28Z","timestamp":1736020288000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11560548_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}