{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:05:01Z","timestamp":1725573901080},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_17","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"286-305","source":"Crossref","is-referenced-by-count":2,"title":["Compilation by Refinement for a Practical Assembly Language"],"prefix":"10.1007","author":[{"given":"Geoffrey","family":"Watson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1016\/0950-5849(90)90174-P","volume":"32","author":"M.A. Ould","year":"1990","unstructured":"Ould, M.A.: Software development under Def Stan 00-55: A guide. Information and Software Technology\u00a032, 170\u2013175 (1990)","journal-title":"Information and Software Technology"},{"key":"17_CR2","series-title":"Real-Time Safety Critical Systems","volume-title":"Towards Verified Systems","year":"1994","unstructured":"Bowen, J. (ed.): Towards Verified Systems. Real-Time Safety Critical Systems, vol.\u00a02. Elsevier, Amsterdam (1994)"},{"key":"17_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J. Back","year":"1998","unstructured":"Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)"},{"key":"17_CR4","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"17_CR5","series-title":"AMAST Series in Computing","doi-asserted-by":"publisher","DOI":"10.1142\/9789812830685","volume-title":"An Algebraic Approach to Compiler Design","author":"A. Sampaio","year":"1997","unstructured":"Sampaio, A.: An Algebraic Approach to Compiler Design. AMAST Series in Computing, vol.\u00a04. World Scientific, Singapore (1997)"},{"key":"17_CR6","volume-title":"2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing","author":"C.J. Fidge","year":"1997","unstructured":"Fidge, C.J.: Modelling program compilation in the refinement calculus. In: Duke, D.J., Evans, A.S. (eds.) 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer, Heidelberg (1997), http:\/\/www.bcs.org\/ewic\/"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M\u00fcller-Olm, M.: Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction. LNCS, vol.\u00a01283. Springer, Heidelberg (1997)"},{"key":"17_CR8","first-page":"142","volume-title":"Formal Methods Pacific 1997","author":"K. Lermer","year":"1997","unstructured":"Lermer, K., Fidge, C.J.: Compilation as refinement. Groves, L. and Reeves, S. (eds.). In: Formal Methods Pacific 1997, pp. 142\u2013164. Springer, Heidelberg (1997)"},{"key":"17_CR9","unstructured":"ECMA standardization - original submission, Web: http:\/\/msdn.microsoft.com\/net\/ecma\/OctoberSubmission.asp (accessed November 1, 2002)"},{"key":"17_CR10","volume-title":".NET Framework Essentials","author":"H. Lam","year":"2001","unstructured":"Lam, H., Thai, T.: .NET Framework Essentials. O\u2019Reilly & Associates, Sebastopol (2001)"},{"key":"17_CR11","unstructured":"Platt, D.S.: Introducing Microsoft .NET. Microsoft Press (2001)"},{"key":"17_CR12","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1989","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall International Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1989)","edition":"2"},{"key":"17_CR13","first-page":"33","volume-title":"3rd Refinement Workshop","author":"C.A.R. Hoare","year":"1990","unstructured":"Hoare, C.A.R.: Refinement algebra proves correctness of compiling specifications. In: Morgan, C., Woodcock, J. (eds.) 3rd Refinement Workshop, pp. 33\u201348. Springer, Heidelberg (1990)"},{"key":"17_CR14","series-title":"Lecture Notes of International Summer School at Marktoberdorf","volume-title":"Refinement algebra proves correctness of a compiler","author":"C.A.R. Hoare","year":"1990","unstructured":"Hoare, C.A.R., Jifeng, H.: Refinement algebra proves correctness of a compiler. Lecture Notes of International Summer School at Marktoberdorf. Springer, Heidelberg (1990)"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1093\/comjnl\/39.1.52","volume":"39","author":"E. B\u00f6rger","year":"1996","unstructured":"B\u00f6rger, E., Durdanovi\u0107, I.: Correctness of compiling Occam to transputer code. The Computer Journal\u00a039, 52\u201392 (1996)","journal-title":"The Computer Journal"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-57877-3_20","volume-title":"Compiler Construction","author":"M. Fr\u00e4nzle","year":"1994","unstructured":"Fr\u00e4nzle, M., M\u00fcller-Olm, M.: Towards provably correct code generation for a hard real-time programming language. In: Fritzson, P.A. (ed.) CC 1994. LNCS, vol.\u00a0786, pp. 294\u2013308. Springer, Heidelberg (1994)"},{"key":"17_CR17","unstructured":"Olderog, E.-R.: ProCoS tutorial: Specifications to programs. In: Formal Methods Europe 1993 Tutorial Material, Odense, Denmark, April 1993, pp. 422\u2013436 (1993)"},{"key":"17_CR18","volume-title":"Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers","author":"H. Jifeng","year":"1995","unstructured":"Jifeng, H.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. McGraw-Hill, New York (1995)"},{"key":"17_CR19","unstructured":"Coglio, A., Goldberg, A., Qian, Z.: Towards a provably-correct implementation of the JVM bytecode verifier. In: Proc. OOPSLA 1998 Workshop on Formal Underpinnings of Java (October 1998)"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1002\/cpe.597","volume":"13","author":"G. Klein","year":"2001","unstructured":"Klein, G., Nipkow, T.: Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience\u00a013, 1133\u20131151 (2001)","journal-title":"Concurrency and Computation : Practice and Experience"},{"key":"17_CR21","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0167-6423(90)90024-8","volume":"14","author":"C. Morgan","year":"1990","unstructured":"Morgan, C., Vickers, T.: Types and invariants in the refinement calculus. Science of Computer Programming\u00a014, 281\u2013304 (1990)","journal-title":"Science of Computer Programming"},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(01)00047-0","volume":"282","author":"K. Lermer","year":"2002","unstructured":"Lermer, K., Fidge, C.J.: A formal model of real-time program compilation. Theoretical Computer Science\u00a0282, 151\u2013190 (2002)","journal-title":"Theoretical Computer Science"},{"key":"17_CR24","unstructured":"TC39 - programming and scripting languages, Web: http:\/\/www.ecma.ch\/ecma1\/memento\/TC39-G3.htm (acc. November 1 2002)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Syme, D.: Typing a multi-language intermediate code. Tech. Rep. MSR-TR-2000-106, MicroSoft Corporation (2000)","DOI":"10.1145\/360204.360228"},{"key":"17_CR26","volume-title":"High Integrity Compilation: A Case Study","author":"S. Stepney","year":"1993","unstructured":"Stepney, S.: High Integrity Compilation: A Case Study. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Crary, K., Walker, D., Glew, N.: Stack-based typed assembly language. Journal of Functional Programming (2002)","DOI":"10.1017\/S0956796801004178"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0055755","volume-title":"Mathematical Foundations of Computer Science 1998","author":"E. B\u00f6rger","year":"1998","unstructured":"B\u00f6rger, E., Schulte, W.: Defining the Java virtual machine as platform for provably correct Java compilation. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, p. 17. Springer, Heidelberg (1998)"},{"key":"17_CR29","unstructured":"Mannasse, M.S., Nelson, G.: Correct comilation of control structures. Tech. rep., AT&T Bell Laboratories (1984)"},{"key":"17_CR30","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Back, R.-J.R.: Refinement of parallel and reactive programs. Tech. Rep. Caltech-CS-TR-92-23, California Institute of Technology (1992)","DOI":"10.1007\/978-3-662-02880-3_3"},{"key":"17_CR32","unstructured":"Microsoft Corporation, Microsoft _ Language Specifications. Microsoft Press (2001)"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-45614-7_28","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L. Wildman","year":"2002","unstructured":"Wildman, L.: A formal basis for a program compilation proof tool. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 491\u2013510. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T19:46:40Z","timestamp":1685908000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}