{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:49Z","timestamp":1725467509445},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055127","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"17-32","source":"Crossref","is-referenced-by-count":2,"title":["Extending window inference"],"prefix":"10.1007","author":[{"given":"Joakim","family":"von Wright","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"2_CR1","first-page":"125","volume-title":"Refinement diagrams","author":"R. J. Back","year":"1991","unstructured":"R. J. Back. Refinement diagrams. In J.M. Morris and R.C.F. Shaw, editors, Proc. 4th Refinement Workshop, Workshops in Computer Science, pages 125\u2013137, Cambridge, England, 9\u201311 January 1991. Springer-Verlag."},{"key":"2_CR2","unstructured":"R. J. Back, J. Grundy, and J. von Wright. Structured calculational proof. Tech. Rpt. 65, Turku Centre for Computer Science, November 1996. to appear in Formal Aspects of Computing."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"R. J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"2_CR4","unstructured":"H. Becht, A. Bloesch, R. Nickson and I. Hayes. Ergo 4.1 Reference Manual. Tech.Rpt. 96-31, Dept. Computer Science, Queensland University, November 1996."},{"key":"2_CR5","volume-title":"Discrete Mathematics and Theoretical Computer Science","author":"M. J. Butler","year":"1997","unstructured":"M. J. Butler, J. Grundy, T. L\u00e5ngbacka, R. Ruksenas, and J. von Wright. The refinement calculator: Proof support for program refinement. In Proc. FMP'97 \u2014 Formal Methods Pacific, Discrete Mathematics and Theoretical Computer Science, Wellington, New Zealand, July 1997. Springer-Verlag."},{"key":"2_CR6","volume-title":"Introduction to HOL","author":"M. J. C. Gordon","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, New York, 1993."},{"key":"2_CR7","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."},{"key":"2_CR8","series-title":"Tech. Rpt. 318","volume-title":"PhD thesis","author":"J. Grundy","year":"1993","unstructured":"J. Grundy. A Method of Program Refinement. PhD thesis, University of Cambridge Computer Laboratory, Cambridge, England, 1993. Tech. Rpt. 318."},{"issue":"4","key":"2_CR9","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1093\/comjnl\/39.4.291","volume":"39","author":"J. Grundy","year":"1996","unstructured":"J. Grundy. Transformational Hierarchical Reasoning. The Computer Journal, 39(4):291\u2013302, 1996.","journal-title":"The Computer Journal"},{"key":"2_CR10","volume-title":"The minimal user-interface of a simple refinement tool","author":"P. Heuberger","year":"1997","unstructured":"P. Heuberger. The minimal user-interface of a simple refinement tool. In Proc. 3rd Workshop on User Interfaces for Theorem Provers, INRIA Sophia-Antipolis, September 1997."},{"key":"2_CR11","unstructured":"R. Nickson. Window inference for data refinement. In Proc. 5th Australasian Refinement Workshop, University of Queensland, 1996."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"R. Nickson and I. Hayes. Supporting contexts in program refinement. Tech.Rpt. 96-29, Dept. Computer Science, Queensland University, 1996.","DOI":"10.1016\/S0167-6423(97)00002-6"},{"issue":"1","key":"2_CR13","doi-asserted-by":"crossref","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 a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1):47\u201361, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"2_CR14","unstructured":"M. Staples. Window inference in Isabelle. In Proc. Isabelle Users Workshop, University of Cambridge Computer Laboratory, September 1995."},{"key":"2_CR15","unstructured":"M. Utting. The Ergo 5 Generic Proof Engine. Tech.Rpt. 97-44, Dept. Computer Science, Queensland University, 1997."}],"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\/BFb0055127","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:34:00Z","timestamp":1555749240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055127"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0055127","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}