{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:45Z","timestamp":1725664005415},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_55","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:11:16Z","timestamp":1330272676000},"page":"378-390","source":"Crossref","is-referenced-by-count":3,"title":["Simplifying deep embedding: A formalised code generator"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Reetz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"25_CR1","first-page":"384","volume-title":"HOL Theorem Proving System and its Applications","author":"E. Barros Lucena de","year":"1991","unstructured":"E. de Barros Lucena. Reasoning about petri nets in HOL. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 384\u2013394, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press."},{"key":"25_CR2","first-page":"253","volume-title":"HOL Theorem Proving System and its Applications","author":"P. Curzon","year":"1991","unstructured":"P. Curzon. A verified compiler for a structured assembly language. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 253\u2013262, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press."},{"key":"25_CR3","volume-title":"HUG93, HOL User's Group Workshop","author":"E. Gunter","year":"1993","unstructured":"E. Gunter. A broader class of trees for recursive type definitions for HOL. In HUG93, HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag."},{"key":"25_CR4","unstructured":"J.E. Hopcroft and J.D. Ullman. Introduction to automata theory, languages, and computation. Addison Wesley, 1979."},{"key":"25_CR5","first-page":"242","volume-title":"HOL Theorem Proving System and its Applications","author":"D.F. Martin","year":"1991","unstructured":"D.F. Martin and R.J. Toal. Case studies in compiler correctness using HOL. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 242\u2013252, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press."},{"key":"25_CR6","volume-title":"Technical Report 244","author":"T.F. Melham","year":"1992","unstructured":"T.F. Melham. A mechanized theory of the \u03c0-calculus in HOL. Technical Report 244, University of Cambridge, Computer Laboratory, Cambridge, England, January 1992."},{"key":"25_CR7","first-page":"193","volume-title":"Rechnergestuetzter Entwurf und Architektur mikroelektronischer Systeme","author":"R. Reetz","year":"1994","unstructured":"R. Reetz and Th. Kropf. Formalisierung eines Flussgraphmodells in Logik hoeherer Ordnung und dessen Anwendung in der Hardware-Verifikation. In D. Monjau, editor, Rechnergestuetzter Entwurf und Architektur mikroelektronischer Systeme, pages 193\u2013202, Oberwiesenthal, Germany, May 1994. Gesellschaft fuer Informatik e.V. (GI)."},{"key":"25_CR8","unstructured":"R. Ripken. Generating an intermediate-code generator in a compiler-writing system. In E. Gelenbe and D. Potier, editors, International Computing Symposium, pages 121\u2013127. North Holland, 1975."},{"key":"25_CR9","unstructured":"IEEE standard VHDL language reference manual. Std 1076, IEEE, 1987."},{"key":"25_CR10","volume-title":"HUG93, HOL User's Group Workshop","author":"C. Zhang","year":"1993","unstructured":"C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson. Mechanizing a programming logic for the concurrent programming language microSR in HOL. In HUG93, HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag."}],"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-58450-1_55.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:16:13Z","timestamp":1619572573000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_55"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_55","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}