{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:30:12Z","timestamp":1759991412258},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_28","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"491-510","source":"Crossref","is-referenced-by-count":4,"title":["A Formal Basis for a Program Compilation Proof Tool"],"prefix":"10.1007","author":[{"given":"Luke","family":"Wildman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"C. J. Fidge. Modelling program compilation in the refinement calculus. In D. J. Duke and A. S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer-Verlag, 1997.","DOI":"10.14236\/ewic\/FA1997.8"},{"key":"28_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"Markus M\u00fcller-Olm. Modular Compiler Verification, volume 1283 of LNCS. Springer, 1997."},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"A. Sampaio. An Algebraic Approach to Compiler Design, volume 4 of AMAST Series in Computing. World Scientific, 1997.","DOI":"10.1142\/2870"},{"key":"28_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0000505","volume-title":"Algebraic Methodology and Software Technology (AMAST\u201997)","author":"O. Traynor","year":"1997","unstructured":"O. Traynor, D. Hazel, P. Kearney, A. Martin, R. Nickson, and L. Wildman. The Cogito development system. In M. Johnson, editor, Algebraic Methodology and Software Technology (AMAST\u201997), volume 1349 of LNCS. Springer-Verlag, December 1997."},{"key":"28_CR5","unstructured":"A. Bloesch, E. Kazmierczak, P. Kearney, J. Staples, O. Traynor, and M. Utting. A formal reasoning environment for Sum-a Z based specification language. In Kotagiri Ramamohanarao, editor, Proceedings of the Nineteenth Australasian Computer Science Conference (ACSC\u201996). Australian Computer Science Communications, 1996."},{"key":"28_CR6","unstructured":"P. Kearney and L. Wildman. From formal specifications to Ada programs. In J. Edwards, editor, Computer Science: Proc. of the 22nd Australasian Computer Science Conference (ACSC\u201999), pages 193\u2013204. Springer, 1999."},{"key":"28_CR7","unstructured":"ECMA TC39\/TG3. ECMA standardisation. http:\/\/msdn.microsoft.com\/net\/ecma ."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Mark B. Josephs. The data refinement calculator for Z specifications. Information Processing Letters, 27, February 1988.","DOI":"10.1016\/0020-0190(88)90078-6"},{"key":"28_CR9","unstructured":"Jim Woodcock and Jim Davies. Using Z, Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall, 1996."},{"key":"28_CR10","unstructured":"C. Morgan. Programming from Specifications. International Series in Computer Science. Prentice Hall, 2nd edition, 1995."},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Mathematics of Program Construction, Second International Conference, Oxford, U.K.","author":"E. Sekerinski","year":"1993","unstructured":"Emil Sekerinski. A calculus for predicative programming. In R.S. Bird, C.C. Morgan, and J.C.P. Woodcock, editors, Mathematics of Program Construction, Second International Conference, Oxford, U.K., volume 669 of LNCS. Springer-Verlag, New York, N.Y., June\/July 1993."},{"key":"28_CR12","unstructured":"A. Martin, R. Nickson, and M. Utting. A tactic language for Ergo. In Proceedings Formal Methods Pacific (FMP\u201997). Springer-Verlag."},{"key":"28_CR13","unstructured":"D.T. Jordan, C.J. Locke, J.A. McDermid, C.E. Parker, B.A. Sharp, and I. Toyn. Literate Formal Development of Ada from Z for Safety Critical Applications. In SAFECOMP, 1994."},{"key":"28_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-52513-0_10","volume-title":"VDM and Z-Formal Methods in Software Development","author":"S. King","year":"1990","unstructured":"S. King. Z and the refinement calculus. In VDM and Z-Formal Methods in Software Development, LNCS 428, pages 164\u2013188. Springer-Verlag, 1990."},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"John Staples, Peter J. Robinson, and Daniel Hazel. A functional logic for higher level reasoning about computation. Formal Aspects of Computing, BCS, 6, 1996.","DOI":"10.1007\/BF01211079"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"K. Lermer and C. J. Fidge. A formal model of real-time program compilation. Theoretical Computer Science, 2001. In press.","DOI":"10.1016\/S0304-3975(01)00047-0"},{"key":"28_CR17","unstructured":"K. Lermer and C. J. Fidge. Compilation as refinement. In L. Groves and S. Reeves, editors, In Proceedings Formal Methods Pacific (FMP\u201997). Springer-Verlag, 1997."},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"T.S. Norvell. Machine code programs are predicates too. In D. Till, editor, sixth refinement workshop. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3240-0_10"},{"key":"28_CR19","series-title":"Lect Notes Comput Sci","volume-title":"First International Symposium of Formal Methods Europe FME\u201993","author":"N. Ward","year":"1993","unstructured":"Nigel Ward. Adding specification constructors to the refinement calculus. In J. P. Woodcock and P. G. Larsen, editors, First International Symposium of Formal Methods Europe FME\u201993, volume 670 of LNCS, Odense, Denmark, April 1993. Springer-Verlag."},{"key":"28_CR20","unstructured":"G. Smith. Stepwise development from ideal specifications. In J. Edwards, editor, Australasian Computer Science Conference, Los Alamitos, California, January 2000. IEEE Computer Society."},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"R. Nickson and I. Hayes. Supporting contexts in program refinement. Science of Computer Programming 29, 1997.","DOI":"10.1016\/S0167-6423(97)00002-6"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"P.J. Robinson and J. Staples. Formalising the hierachical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1), 1993.","DOI":"10.1093\/logcom\/3.1.47"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"28_CR24","unstructured":"Ray Nickson. Window inference for data refinement. In Fifth Australasian Refinement Workshop, University of Queensland, April 1996."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:05:04Z","timestamp":1683842704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}