{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:05:36Z","timestamp":1725663936076},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540559849"},{"type":"electronic","value":"9783540473350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55984-1_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:49:29Z","timestamp":1330235369000},"page":"141-155","source":"Crossref","is-referenced-by-count":10,"title":["Provably correct compiler development and implementation"],"prefix":"10.1007","author":[{"given":"Bettina","family":"Buth","sequence":"first","affiliation":[]},{"given":"Karl-Heinz","family":"Buth","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Burghard","family":"Karger","sequence":"additional","affiliation":[]},{"given":"Yassine","family":"Lakhneche","sequence":"additional","affiliation":[]},{"given":"Hans","family":"Langmaack","sequence":"additional","affiliation":[]},{"given":"Markus","family":"M\u00fcller-Olm","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"14_CR1","volume-title":"Final Deliverable of the ProCoS Project","author":"D. Bj\u00f8rner","year":"1992","unstructured":"Dines Bj\u00f8rner et al. Final Deliverable of the ProCoS Project. Computer Science Department, Technical University of Denmark, Lyngby, DK, 1992 (submitted to Springer Verlag for publication)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Dines Bj\u00f8rner, Cliff B. Jones. The Vienna Development Method: The Meta Language. LNCS 61. Springer Verlag, 1978","DOI":"10.1007\/3-540-08766-4"},{"key":"14_CR3","unstructured":"R.S. Boyer, J S. Moore. A Computational Logic Handbook. Academic Press, 1988"},{"key":"14_CR4","volume-title":"Master's Thesis","author":"M. Fr\u00e4nzle","year":"1990","unstructured":"Martin Fr\u00e4nzle. Verification of Compilers for Recursive occam-like Languages. Master's Thesis, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, FRG, 1990"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall Int., 1985","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"14_CR6","volume-title":"PRG-TR-6-90","author":"C.A.R. Hoare","year":"1990","unstructured":"C.A.R. Hoare. Refinement Algebra Proves Correctness of Compiling Specifications. PRG-TR-6-90. Programming Research Group, Oxford University, UK, 1990"},{"key":"14_CR7","unstructured":"inmos Limited. Transputer instruction set: A compiler writers guide. Prentice-Hall Int., 1988"},{"key":"14_CR8","unstructured":"inmos Limited. occam 2 Reference Manual. Prentice-Hall Int., 1988"},{"key":"14_CR9","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall Int., 1990"},{"key":"14_CR10","volume-title":"Master's Thesis","author":"Y. Lakhneche","year":"1991","unstructured":"Yassine Lakhneche. Equivalence of Denotational and Structural Operational Semantics of PL. Master's Thesis, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, FRG, 1991"},{"key":"14_CR11","volume-title":"Master's Thesis","author":"M. M\u00fcller-Olm","year":"1990","unstructured":"Markus M\u00fcller-Olm. Correctness Proof of SubLISP to PL Translation. Master's Thesis, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, FRG, 1990"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"W. Polak. Compiler Specification and Verification. LNCS 124. Springer Verlag, 1981","DOI":"10.1007\/3-540-10886-6"},{"key":"14_CR13","unstructured":"Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"W.D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5(4), December 1989","DOI":"10.1007\/BF00243134"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55984-1_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:21:13Z","timestamp":1687270873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55984-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540559849","9783540473350"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-55984-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}