{"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":1725663824362},"publisher-location":"Berlin, Heidelberg","reference-count":22,"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_127","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:27:13Z","timestamp":1330262833000},"page":"89-100","source":"Crossref","is-referenced-by-count":2,"title":["Degrees of formality in shallow embedding hardware description languages in HOL"],"prefix":"10.1007","author":[{"given":"Catia M.","family":"Angelo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luc","family":"Claesen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hugo","family":"Man","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"M. Gordon. \u201cHOL: A Proof Generating System for Higher-Order Logic\u201d. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"7_CR2","first-page":"129","volume-title":"Experience with Embedding Hardware Description Languages in HOL","author":"R. Boulton","year":"1992","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel. \u201cExperience with Embedding Hardware Description Languages in HOL\u201d. In V. Stavridou, T.F. Melham, and R. Boute, editors, Proceedings of the IFIP International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129\u2013156. Nijmegen, The Netherlands, North-Holland, Amsterdam, June 1992."},{"key":"7_CR3","first-page":"27","volume-title":"Using Recursive Types to Reason about Hardware in Higher Order Logic","author":"T.F. Melham","year":"1988","unstructured":"T.F. Melham. \u201cUsing Recursive Types to Reason about Hardware in Higher Order Logic\u201d. In G.J. Milne, editor, The Fusion of Hardware Design and Verification: Proceedings of the IFIP WG 10.2 Working Conference, pages 27\u201350. Glasgow, North-Holland, Amsterdam, July 1988."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"T.F. Melham. \u201cAutomating Recursive Type Definitions in Higher Order Logic\u201d. In G. 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":"7_CR5","volume-title":"The ML Handbook","author":"G. Cousineau","year":"1986","unstructured":"G. Cousineau, M. Gordon, G. Huet, R. Milner, L. Paulson, and C. Wadsworth. The ML Handbook. INRIA, France, 1986."},{"key":"7_CR6","first-page":"561","volume-title":"Why We Can't Have SML Style Datatype Declarations in HOL","author":"E.L. Gunter","year":"1992","unstructured":"E.L. Gunter. \u201cWhy We Can't Have SML Style Datatype Declarations in HOL\u201d. In L. Claesen and M. Gordon, editors, Proceedings of the IFIP International Workshop on Higher Order Logic Theorem Proving and its Applications \u2014 HOL-92, pages 561\u2013568. IMEC, Leuven, Belgium, Elsevier Science Publishers B. V. (North-Holland), Amsterdam, September 1992."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. \u201cThe HOL Verification of ELLA Designs\u201d. In Proceedings of the ACM\/SIGDA International Workshop in Formal Methods in VLSI Design. Miami, FL, January 1991.","DOI":"10.1145\/126990.126995"},{"key":"7_CR8","unstructured":"R. Boulton. A HOL Semantics for a Subset of ELLA. Technical Report 254, University of Cambridge Computer Laboratory, April 1992."},{"key":"7_CR9","unstructured":"A.D. Gordon. A Mechanised Definition of Silage in HOL. Technical Report 287, University of Cambridge Computer Laboratory, February 1993."},{"key":"7_CR10","first-page":"531","volume-title":"The Formal Definition of a Synchronous Hardware-description Language in Higher Order Logic","author":"A.D. Gordon","year":"1992","unstructured":"A.D. Gordon. \u201cThe Formal Definition of a Synchronous Hardware-description Language in Higher Order Logic\u201d. In ICCD92: 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors, pages 531\u2013534. Cambridge, Massachusetts, IEEE Computer Society Press, October 1992."},{"key":"7_CR11","first-page":"375","volume-title":"The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL","author":"C.M. Angelo","year":"1992","unstructured":"C.M. Angelo, L. Claesen, and H. De Man. \u201cThe Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL\u201d. In L. Claesen and M. Gordon, editors, Proceedings of the IFIP International Workshop on Higher Order Logic Theorem Proving and its Applications \u2014 HOL-92, pages 375\u2013394. IMEC, Leuven, Belgium, Elsevier Science Publishers B. V. (North-Holland), Amsterdam, September 1992."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"J. Van Tassel. A Formalisation of the VHDL Simulation Cycle. Technical Report 249, University of Cambridge Computer Laboratory, March 1992.","DOI":"10.1016\/B978-0-444-89880-7.50029-2"},{"key":"7_CR13","first-page":"359","volume-title":"A Formalisation of the VHDL Simulation Cycle","author":"J. Tassel Van","year":"1992","unstructured":"J. Van Tassel. \u201cA Formalisation of the VHDL Simulation Cycle\u201d. In L. Claesen and M. Gordon, editors, Proceedings of the IFIP International Workshop on Higher Order Logic Theorem Proving and its Applications \u2014 HOL-92, pages 359\u2013374. IMEC, Leuven, Belgium, Elsevier Science Publishers B. V. (North-Holland), Amsterdam, September 1992."},{"key":"7_CR14","unstructured":"P.N. Hilfinger. \u201cSilage, a High-level Language and Silicon Compiler for Digital Signal Processing\u201d. In Proceedings of the IEEE 1985 Custom Integrated Circuits Conference \u2014 CICC-85, pages 213\u2013216. Portland, OR, May 1985."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"P.N. Hilfinger. Silage Reference Manual, December 1987.","DOI":"10.1049\/esn.1987.0025"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"D. Genin, P.N. Hilfinger, J. Rabaey, C. Scheers, and H. De Man. \u201cDSP Specification Using the Silage Language\u201d. In Proceedings of the IEEE International Conference on Accoustics, Speech and Signal Processing, pages 1057\u20131060. Albuquerque, NM, April 1990.","DOI":"10.1109\/ICASSP.1990.116097"},{"key":"7_CR17","volume-title":"A Silage Tutorial","author":"L. Nachtergaele","year":"1990","unstructured":"L. Nachtergaele. A Silage Tutorial. IMEC, Leuven, Belgium, May 1990."},{"key":"7_CR18","volume-title":"User Manual for the S2C Silage to C Compiler","author":"L. Nachtergaele","year":"1990","unstructured":"L. Nachtergaele. User Manual for the S2C Silage to C Compiler. IMEC, Leuven, Belgium, May 1990."},{"issue":"6","key":"7_CR19","first-page":"73","volume":"3","author":"H. Man De","year":"1986","unstructured":"H. De Man, J. Rabaey, P. Six, and L. Claesen. \u201cCathedral-II: a Silicon Compiler for Digital Signal Processing\u201d. IEEE Design & Test of Computers, 3(6):73\u201385, December 1986.","journal-title":"IEEE Design & Test of Computers"},{"key":"7_CR20","volume-title":"Technical report","author":"P. Lippens","year":"1988","unstructured":"P. Lippens. Defining Control Flow from an Applicative Specification. Technical report, Philips Research Laboratories, Eindhoven, December 1988."},{"key":"7_CR21","volume-title":"PhD thesis","author":"I. Verbauwhede","year":"1991","unstructured":"I. Verbauwhede. VLSI Design Methodologies for Application-specific Cryptographic and Algebraic Systems. PhD thesis, Katholieke Universiteit Leuven \u2014 IMEC, Leuven, Belgium, 1991."},{"key":"7_CR22","volume-title":"Technical report","author":"J. Vanhoof","year":"1992","unstructured":"J. Vanhoof. Multi-rate Expansion for CATHEDRAL-II\/III. A tutorial. Technical report, IMEC, Leuven, Belgium, October 1992."}],"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_127.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:25Z","timestamp":1605647665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_127"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_127","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}