{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:47:58Z","timestamp":1770274078402,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105399","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"93-108","source":"Crossref","is-referenced-by-count":9,"title":["Program derivation using the refinement calculator"],"prefix":"10.1007","author":[{"given":"Michael","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"L\u00e5ngbacka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"7_CR1","volume-title":"A Theorem Prover for UNITY in Higher Order Logic","author":"F. Andersen","year":"1992","unstructured":"F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, Lyngby, 1992."},{"key":"7_CR2","volume-title":"Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts","author":"R. Back","year":"1980","unstructured":"R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980."},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R. Back","year":"1988","unstructured":"R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593\u2013624, 1988.","journal-title":"Acta Informatica"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"R. Back","year":"1990","unstructured":"R. Back and J. von Wright. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 2:247\u2013272, 1990.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR5","unstructured":"M. Butler, T. L\u00e5ngbacka, R. Ruk\u0161\u0117nas, and J. von Wright. Refinement Calculator tutorial and manual. Draft \u2014 available upon request."},{"issue":"9","key":"7_CR6","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A. Camillieri","year":"1990","unstructured":"A. Camillieri. Mechanizing CSP trace theory in Higher Order Logic. IEEE Transactions on Software Engineering, 16(9):993\u20131004, 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. A tool for developing correct programs by refinement. For presentation at 7th BCS-FACS Refinement Workshop, July 1996.","DOI":"10.14236\/ewic\/RW1996.3"},{"key":"7_CR8","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"J. Grundy. Window inference in the HOL system. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, pages 177\u2013189, University of California at Davis, August 1991. ACM-SIGDA, IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596285"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"J. Grundy. A window inference tool for refinement. In Jones et al, editor, Proc. 5th Refinement Workshop, London, Jan. 1992. Springer-Verlag.","DOI":"10.1007\/978-1-4471-3550-0_12"},{"key":"7_CR11","unstructured":"J. Grundy. HOL90 window library manual. 1994."},{"key":"7_CR12","unstructured":"T. L\u00e5ngbacka. TkWinHOL users guide. Draft \u2014 available upon request."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"T. L\u00e5ngbacka, R. Ruk\u0161\u0117nas, and J. von Wright. TkWinHOL: A tool for doing window inference in HOL. In Schubert et al. [17], pages 245\u2013260.","DOI":"10.1007\/3-540-60275-5_69"},{"key":"7_CR14","unstructured":"C.C. Morgan. Programming from Specifications (2nd Edition). Prentice-Hall, 1994."},{"issue":"3","key":"7_CR15","doi-asserted-by":"crossref","first-page":"298","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. Sci. Comp. Prog., 9(3):298\u2013306, 1987.","journal-title":"Sci. Comp. Prog."},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P.J. Robinson","year":"1993","unstructured":"P.J. Robinson and J. Staples. Formalising the hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1):47\u201361, February 1993.","journal-title":"Journal of Logic and Computation"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, editors. Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Science, Aspen Grove, Utah, September 1995. Springer-Verlag.","DOI":"10.1007\/3-540-60275-5"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"D. Syme. A new interface for HOL \u2014 ideas, issues and implementation. In Schubert et al. [17], pages 324\u2013339.","DOI":"10.1007\/3-540-60275-5_74"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"L. Th\u00e9ry. A Proof Development System for the HOL Theorem Prover. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications \u2014 6th International Workshop, HUG\u2019 93 Vancouver, B. C., Canada, August 1993, volume 780 of Lecture Notes in Computer Science, pages 115\u2013128. Springer Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_129"},{"key":"7_CR20","unstructured":"M. Utting and K. Whitwell. Ergo user manual. Technical Report 93-19, Software Verification Research Centre, University of Queensland, 1994."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"J. von Wright. Program refinement by theorem prover. In BCS FACS Sixth Refinement Workshop \u2014 Theory and Practise of Formal Software Development. 5th\u20137th January, City University, London, UK., 1994.","DOI":"10.1007\/978-1-4471-3240-0_7"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J. Wright von","year":"1993","unstructured":"J. von Wright, J. Hekanaho, P. Luostarinen, and T. L\u00e5ngbacka. Mechanising some advanced refinement concepts. Formal Methods in Systems Design, 3:49\u201381, 1993.","journal-title":"Formal Methods in Systems Design"}],"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\/BFb0105399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T09:22:46Z","timestamp":1593249766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105399"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0105399","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}