{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:01Z","timestamp":1725664921567},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_69","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:06:00Z","timestamp":1330279560000},"page":"245-260","source":"Crossref","is-referenced-by-count":6,"title":["TkWinHOL: A tool for Window Inference in HOL"],"prefix":"10.1007","author":[{"given":"Thomas","family":"L\u00e5ngbacka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rimvydas","family":"Ruk\u0161\u0117nas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joakim","family":"Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"17_CR1","volume-title":"PhD thesis","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":"17_CR2","volume-title":"volume 859 of Lecture Notes in Computer Science","author":"F. Andersen","year":"1994","unstructured":"Flemming Andersen, Kim Dam Petersen, and Jimmi S. Petterson. A Graphical Tool for Proving UNITY Progress. In T. F. Melham and J. Camilleri, editors, Higher Order Logic Theorem Proving and Its Applications \u2014 7th International Workshop. Valletta, Malta, September 1994, volume 859 of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"17_CR3","volume-title":"volume 131 of Mathematical Center Tracts","author":"R.J.R. 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":"17_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":"17_CR5","unstructured":"R. J. R. Back, J. Hekanaho and K. Sere. Centipede \u2014 a Program Refinement Environment, Reports on Computer Science and Mathematics, Ser. A 139, \u00e5bo Akademi University, 1992."},{"key":"17_CR6","volume-title":"volume 430 of Lecture Notes in Computer Science","author":"R.J.R. Back","year":"1989","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-Verlag."},{"key":"17_CR7","doi-asserted-by":"crossref","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:247\u2013272, 1990.","journal-title":"Formal Aspects of Computing"},{"issue":"9","key":"17_CR8","doi-asserted-by":"crossref","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":"17_CR9","unstructured":"E.W. Dijkstra A Discipline of Programming. Prentice-Hall, 1976."},{"key":"17_CR10","unstructured":"M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL. Cambridge University Press, 1993."},{"key":"17_CR11","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":"17_CR12","unstructured":"J. Grundy. HOL90 window library manual. 1994."},{"key":"17_CR13","first-page":"174","volume-title":"volume 780 of Lecture Notes in Computer Science","author":"J. Harrison","year":"1993","unstructured":"John Harrison and Laurent Th\u00e9ry. Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications \u2014 6th International Workshop, HUG '93 Vancouver, B. C., Canada, August 1993, volume 780 of Lecture Notes in Computer Science, pages 174\u2013184. Springer Verlag, 1993."},{"key":"17_CR14","unstructured":"Don Libes. Exploring Expect: A Tcl-based Toolkit for Automating Interactive Programs. O'Reilly & Associates, 1994."},{"key":"17_CR15","unstructured":"John K. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994."},{"key":"17_CR16","unstructured":"Thomas W. Reps and Tim Teitelbaum, editors. The Synthesizer Generator. A System for Constructing Language-Based Editors. Springer-Verlag, 1988."},{"key":"17_CR17","volume-title":"Techn. Rep. 138","author":"P.J. 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":"17_CR18","unstructured":"Donald Syme. A New Interface for HOL \u2014 Ideas, Issues and Implementation, submitted to the HUG95."},{"key":"17_CR19","first-page":"115","volume-title":"volume 780 of Lecture Notes in Computer Science","author":"L. Th\u00e9ry","year":"1993","unstructured":"Laurent 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 '93 Vancouver, B. C., Canada, August 1993, volume 780 of Lecture Notes in Computer Science, pages 115\u2013128. Springer Verlag, 1993."},{"key":"17_CR20","doi-asserted-by":"crossref","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"},{"key":"17_CR21","volume-title":"Program refinement by theorem prover","author":"J. Wright von","year":"1994","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."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:35:36Z","timestamp":1619573736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}