{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:32Z","timestamp":1774837832649,"version":"3.50.1"},"publisher-location":"London","reference-count":32,"publisher":"Springer London","isbn-type":[{"value":"9783540198864","type":"print"},{"value":"9781447132400","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/978-1-4471-3240-0_7","type":"book-chapter","created":{"date-parts":[[2011,12,28]],"date-time":"2011-12-28T05:22:09Z","timestamp":1325049729000},"page":"121-150","source":"Crossref","is-referenced-by-count":12,"title":["Program Refinement by Theorem Prover"],"prefix":"10.1007","author":[{"given":"J.","family":"von Wright","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"M. Aagard and M. Leeser. Verifying a logic synthesis tool in Nuprl. In Proc. 4th Workshop on Computer-Aided Verification,Montreal, Canada, June 1992. Springer-Verlag."},{"key":"7_CR2","volume-title":"Aarhus University","author":"S Agerholm","year":"1992","unstructured":"S. Agerholm. Mechanizing program verification in HOL. DAIMI IR-111, Aarhus University, Apr. 1992."},{"key":"7_CR3","volume-title":"A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark","author":"F Andersen","year":"1992","unstructured":"F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, Lyngby, Denmark, Mar. 1992."},{"key":"7_CR4","volume-title":"Amsterdam","author":"RJR Back","year":"1980","unstructured":"R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"RJR 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":"7_CR6","volume-title":"21st Hawaii International Conference on System Sciences","author":"RJR Back","year":"1989","unstructured":"R.J.R. Back. Changing data representation in the refinement calculus. In 21st Hawaii International Conference on System Sciences, January 1989."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"R.J.R. Back. Refinement calculus, part II: Parallel and reactive programs. In REX Workshop for Refinement of Distributed Systems,volume 430 of Lecture Notes in Computer Science,Nijmegen, The Netherlands, 1989. Springer\u2014Verlag.","DOI":"10.1007\/3-540-52559-9_61"},{"key":"7_CR8","volume-title":"K.R. Parker and G.A. Rose, editors, Formal Description Techniques IV, pages 475-493. Elsevier Science Publishers (North-Holland)","author":"RJR Back","year":"1992","unstructured":"R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In K.R. Parker and G.A. Rose, editors, Formal Description Techniques IV, pages 475\u2013493. Elsevier Science Publishers (North-Holland), 1992."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"R.J.R. Back and J. von Wright. Refinement calculus, part I: Sequential programs. In REX Workshop for Refinement of Distributed Systems,volume 430 of Lecture Notes in Computer Science,Nijmegen, The Netherlands, 1989. Springer\u2014Verlag.","DOI":"10.1007\/3-540-52559-9_60"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"RJR Back","year":"1990","unstructured":"R.J.R. Back and J. von Wright. Refinement concepts formalised in higher-order logic. Formal Aspects of Computing, 2: 247\u2013272, 1990.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0167-6423(93)90015-H","volume":"20","author":"RJR Back","year":"1993","unstructured":"R.J.R. Back and J. von Wright. Statement inversion and strongest post-condition Science of Computer Programming, 20: 223\u2013251, 1993.","journal-title":"Science of Computer Programming"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1016\/0304-3975(92)90309-4","volume":"100","author":"RJR Back","year":"1992","unstructured":"R.J.R. Back and J. von Wright. Combining angels, demons and miracles in program specifications. Theoretical Computer Science, 100: 365\u2013383, 1992.","journal-title":"Theoretical Computer Science"},{"issue":"9","key":"7_CR13","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"AJ Camilleri","year":"1990","unstructured":"A.J. Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions of Software Engineering, 16 (9): 993\u20131004, 1990.","journal-title":"IEEE Transactions of Software Engineering"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5: 56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR15","volume-title":"Prentice\u2014Hall International","author":"EW Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice\u2014Hall International, 1976."},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00268074","volume":"23","author":"EW Dijkstra","year":"1986","unstructured":"E.W. Dijkstra and A.J.M. van Gasteren. A simple fixpoint argument without the restriction to continuity. Acta Informatica, 23: 1\u20137, 1986.","journal-title":"Acta Informatica"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"U. Engberg, P. Groenning and L. Lamport. Mechanical verification of concurrent systems with TLA. In Proc. ,nth Workshop on Computer-Aided Verification,Montreal, Canada, June 1992. Springer-Verlag.","DOI":"10.1007\/3-540-56496-9_5"},{"issue":"1","key":"7_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(91)90029-2","volume":"87","author":"PH Gardiner","year":"1991","unstructured":"P.H. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87 (1): 143\u2013162, 1991.","journal-title":"Theoretical Computer Science"},{"key":"7_CR19","first-page":"374","volume-title":"TC2 Working Conference on Programming Concepts and Methods","author":"DM Goldschlag","year":"1990","unstructured":"D. M. Goldschlag. Mechanizing UNITY. In M. Broy, editor, TC2 Working Conference on Programming Concepts and Methods, pages 374\u2013401, Israel, 1990. IFIP."},{"key":"7_CR20","volume-title":"VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers","author":"MJC Gordon","year":"1988","unstructured":"M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam (ed.), VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988."},{"key":"7_CR21","volume-title":"Current Trends in Hardware Verification and Theorem Proving. Springer-Verlag","author":"MJC Gordon","year":"1989","unstructured":"M.J.C. Gordon. Mechanizing programming logics in higher-order logic. In G. Birtwistle and P.A. Subrahmanyam (ed.), Current Trends in Hardware Verification and Theorem Proving. Springer-Verlag, 1989."},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"L. Groves and R. Nickson. A tactic driven refinement tool. In Jones et al, editor, Proc. 5th Refinement Workshop,London, Jan. 1992. Springer\u2014Verlag.","DOI":"10.1007\/978-1-4471-3550-0_14"},{"key":"7_CR23","volume-title":"Proc. 5th Refinement Workshop","author":"J Grundy","year":"1992","unstructured":"J. Grundy. A window inference tool for refinement. In Jones et al, editor, Proc. 5th Refinement Workshop, London, Jan. 1992. Springer-Verlag."},{"issue":"4","key":"7_CR24","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1 (4): 271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"7_CR25","volume-title":"Prentice-Hall International","author":"CB Jones","year":"1986","unstructured":"C.B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986."},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0020-0190(88)90147-0","volume":"26","author":"CC Morgan","year":"1988","unstructured":"C.C. Morgan. Data refinement by miracles. Information Processing Letters, 26: 243\u2013246, January 1988.","journal-title":"Information Processing Letters"},{"key":"7_CR27","volume-title":"Prentice-Hall","author":"CC Morgan","year":"1990","unstructured":"C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990."},{"key":"7_CR28","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00276019","volume":"26","author":"JM Morris","year":"1989","unstructured":"J.M. Morris. Laws of data refinement. Acta Informatica, 26: 287\u2013308, 1989.","journal-title":"Acta Informatica"},{"key":"7_CR29","volume-title":"Techn. Rep","author":"PJ Robinson","year":"1990","unstructured":"P.J. Robinson and J. Staples. Formalising the hierarchical structure of practical mathematical reasoning. Techn. Rep. 138, Key Centre for Software Technology, University of Queensland, Australia, 1990."},{"key":"7_CR30","unstructured":"T. Vickers. An overview of a refinement editor. In 5th Australian Software Engineering Conference, Sydney, May 1990."},{"key":"7_CR31","unstructured":"J. von Wright. The lattice of data refinement. Reports on computer science and mathematics 130, Abo Akademi, 1992. To appear in Acta Informatica."},{"key":"7_CR32","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J von Wright","year":"1993","unstructured":"J. von Wright, J. Hekanaho, P. Luostarinen and T. L\u00e2ngbacka. Mechanising some advanced refinement concepts. Formal Methods in System Design, 3: 49\u201381, 1993.","journal-title":"Formal Methods in System Design"}],"container-title":["Workshops in Computing","6th Refinement Workshop"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3240-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,16]],"date-time":"2024-04-16T19:19:54Z","timestamp":1713295194000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4471-3240-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540198864","9781447132400"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3240-0_7","relation":{},"ISSN":["1431-1682"],"issn-type":[{"value":"1431-1682","type":"print"}],"subject":[],"published":{"date-parts":[[1994]]}}}