{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:25:42Z","timestamp":1725456342135},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633792"},{"type":"electronic","value":"9783540695264"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0028394","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:50:11Z","timestamp":1132642211000},"page":"183-197","source":"Crossref","is-referenced-by-count":3,"title":["Refining reactive systems in HOL using action systems"],"prefix":"10.1007","author":[{"given":"Thomas","family":"L\u00e5ngbacka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joakim","family":"von Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"F. Andersen, K.D. Petersen, and J.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-7th International Workshop. Valletta, Malta, September 1994, volume 859 of Lecture Notes in Computer Science. Springer Verlag, 1994.","key":"13_CR1","DOI":"10.1007\/3-540-58450-1_32"},{"key":"13_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":"13_CR3","doi-asserted-by":"crossref","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":"13_CR4","doi-asserted-by":"crossref","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"},{"doi-asserted-by":"crossref","unstructured":"R. Back and J. von Wright. Trace refinement of action systems. Reports on computer science and mathematics 153, \u00c5bo Akademi, 1994.","key":"13_CR5","DOI":"10.1007\/978-3-540-48654-1_28"},{"doi-asserted-by":"crossref","unstructured":"M. Butler and T. L\u00e5ngbacka. Program derivation using the refinement calculator. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, volume 1125 of Lecture Notes in Computer Science, pages 93\u2013108. Springer Verlag, August 1996.","key":"13_CR6","DOI":"10.1007\/BFb0105399"},{"key":"13_CR7","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"},{"unstructured":"E. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.","key":"13_CR8"},{"key":"13_CR9","first-page":"177","volume-title":"Proceedings of the International Tutorial and Workshop on the HOL Theorem Proving System and its Applications","author":"J. Grundy","year":"1991","unstructured":"J. Grundy. Window inference in the HOL system. In M. Archer, J.J. Joyce, K.N. Levitt, and P.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."},{"unstructured":"R. Ruksenas and J. von Wright. A tool for data refinement. To appear as a TUGS Technical Report, Turku Centre for Computer Science, Lemmink\u00e4isenkatu 14A, 20520 Turku, Finland, 1997.","key":"13_CR10"},{"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 7th January, City University, London, UK., 1994.","key":"13_CR11","DOI":"10.1007\/978-1-4471-3240-0_7"},{"doi-asserted-by":"crossref","unstructured":"J. von Wright and T. L\u00e5ngbacka. Using a theorem prover for reasoning about concurrent algorithms. In G. von Bochmann and D.K. Probst, editors, Computer Aided Verification \u2014 Fourth International Workshop. CAV '92. Montreal. Canada. June 29\u2013July 1. 1992, volume 663 of Lecture Notes in Computer Science. Springer Verlag, 1993.","key":"13_CR12","DOI":"10.1007\/3-540-56496-9_6"}],"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\/BFb0028394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:36:05Z","timestamp":1683297365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633792","9783540695264"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0028394","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}