{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:45Z","timestamp":1725488625573},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_16","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"239-254","source":"Crossref","is-referenced-by-count":2,"title":["Representing WP Semantics in Isabelle\/ZF"],"prefix":"10.1007","author":[{"given":"Mark","family":"Staples","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"16_CR2","unstructured":"S. Agerholm. Mechanizing program verification in HOL. Master\u2019s thesis, Computer Science Department, Aarhus University, April 1992."},{"key":"16_CR3","unstructured":"R. J. R. Back. On the correctness of refinement steps in program development. Technical Report A-1978-4, 0Abo Akademi University, 1978."},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R. J. R. Back","year":"1988","unstructured":"R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593\u2013624, 1988.","journal-title":"Acta Informatica"},{"key":"16_CR5","series-title":"Lect Notes Comput Sci","first-page":"42","volume-title":"Stepwise Refinement of Distributed Systems","author":"R. J. R. Back","year":"1989","unstructured":"R. J. R. Back and J. von Wright. Refinement calculus, part I: Sequential nondeterministic programs. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, pages 42\u201366. Springer-Verlag, 1989."},{"issue":"3","key":"16_CR6","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"R. J. R. Back","year":"1990","unstructured":"R. J. R. Back and J. von Wright. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 2(3):247\u2013272, 1990.","journal-title":"Formal Aspects of Computing"},{"key":"16_CR7","unstructured":"Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, and John Herbert. Experience with embedding hardware description languages. In Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, volume A10 of IFIP Transactions, pages 129\u2013156. North-Holland\/Elsevier, June 1992."},{"key":"16_CR8","unstructured":"D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. Refinement in Ergo. Technical Report 94-44, Software Verification Research Centre, The University of Queensland, July 1995."},{"key":"16_CR9","unstructured":"E. W. Dijkstra. A Discipline of Programming Prentice Hall, 1976."},{"key":"16_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer-Verlag, 1979."},{"key":"16_CR11","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"16_CR12","unstructured":"Thomas Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, Laboratory for Foundations of Computer Science, The University of Edinburgh, September 1998."},{"key":"16_CR13","unstructured":"J. Knappmann. A PVS based tool for developing programs in the refinement calculus. Master\u2019s thesis, Christian-Albrechts-University of Kiel, October 1996."},{"key":"16_CR14","unstructured":"R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990."},{"issue":"1","key":"16_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0167-6423(88)90062-7","volume":"11","author":"C. Morgan","year":"1988","unstructured":"Carroll Morgan. Procedures, parameters, and abstraction: Separate concerns. Science of Computer Programming, 11(1):17\u201328, 1988.","journal-title":"Science of Computer Programming"},{"issue":"3","key":"16_CR16","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C. Morgan","year":"1988","unstructured":"Carroll Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403\u2013419, July 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR17","unstructured":"Carroll Morgan. Programming from Specifications. Prentice-Hall International, 2nd edition, 1994."},{"issue":"3","key":"16_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287\u2013306, December 1987.","journal-title":"Science of Computer Programming"},{"key":"16_CR19","unstructured":"R. G. Nickson and L. J. Groves. Metavariables and conditional refinements in the refinement calculus. Technical Report 93-12, Software Verification Research Centre, The University of Queensland, 1993."},{"key":"16_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994."},{"key":"16_CR21","unstructured":"H. Pfeifer, A. Dold, F. W. von Henke, and H. Rueff. Mechanised semantics of simple imperative programming constructs. Technical Report UIB-96-11, Universit\u00e4t Ulm, December 1996."},{"key":"16_CR22","unstructured":"Chris H. Pratten. Refinement in a Language with Procedures and Modules. PhD thesis, Department of Engineering and Computer Science, University of Southampton, June 1996."},{"key":"16_CR23","unstructured":"Mark Staples. Window inference in Isabelle. In L. Paulson, editor, Proceedings of the First Isabelle User\u2019s Workshop, volume 379, pages 191\u2013205. University of Cambridge Computer Laboratory Technical Report, September 1995."},{"key":"16_CR24","unstructured":"Mark Staples. A Mechanised Theory of Refinement. PhD thesis, Computer Laboratory, University of Cambridge, November 1998. Submitted."},{"key":"16_CR25","unstructured":"M. Utting and K. Whitwell. Ergo user manual. Technical Report 93-19, Software Verification Research Centre, The University of Queensland, February 1994."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"J. von Wright. The lattice of data refinement. Acta Informatica, 31, 1994.","DOI":"10.1007\/BF01192157"},{"key":"16_CR27","unstructured":"J. von Wright. Verifying modular programs in HOL. Technical Report 324, University of Cambridge Computer Laboratory, January 1994."},{"key":"16_CR28","unstructured":"J. von Wright. A Mechanised Calculus of Refinement in HOL, January 27, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T17:51:24Z","timestamp":1550425884000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}