{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:40Z","timestamp":1725664000974},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_52","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:11:42Z","timestamp":1330254702000},"page":"332-345","source":"Crossref","is-referenced-by-count":5,"title":["A HOL formalisation of the Temporal Logic of Actions"],"prefix":"10.1007","author":[{"given":"Thomas","family":"L\u00e5ngbacka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"2","key":"22_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"22_CR2","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":"22_CR3","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":"22_CR4","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":"22_CR5","unstructured":"C-T Chou. Mechanical verification of distributed algorithms in higher-order logic. In these proceedings."},{"key":"22_CR6","unstructured":"U. Engberg, P. Groenning, and L. Lamport. Mechanical verification of concurrent systems with TLA. In G. v. 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":"22_CR7","unstructured":"M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL. Cambridge University Press, 1993."},{"key":"22_CR8","unstructured":"L. Lamport. The temporal logic of actions. Research Report 79, DEC, Systems Research Center, December 1991. A revised version of the paper will appear in ACM Transactions on Programming Languages and Systems."},{"key":"22_CR9","unstructured":"J. von Wright. Mechanising the temporal logic of actions in HOL. In Proceedings of the 1991 HOL Tutorial and Workshop, August 1991."},{"key":"22_CR10","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."},{"key":"22_CR11","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 System Design, 3:49\u201381, 1993.","journal-title":"Formal Methods in System Design"},{"key":"22_CR12","volume-title":"volume 663 of Lecture Notes in Computer Science","author":"J. Wright von","year":"1993","unstructured":"J. von Wright and T. L\u00e5ngbacka. Using a theorem prover for reasoning about concurrent algortihms. In G. v. 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."}],"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-58450-1_52.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:16:12Z","timestamp":1619558172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}