{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:36Z","timestamp":1725663816244},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_123","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:51Z","timestamp":1330262811000},"page":"29-42","source":"Crossref","is-referenced-by-count":2,"title":["Mechanizing a programming logic for the concurrent programming language microSR in HOL"],"prefix":"10.1007","author":[{"given":"Cui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Shaw","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronald A.","family":"Olsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Levitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Myla","family":"Archer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark R.","family":"Heckman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregory D.","family":"Benson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/42192.42324","volume":"10","author":"G.R. Andrews","year":"1988","unstructured":"G.R. Andrews, R.A. Olsson, M. Coffin, I.J.P. Elshoff, K. Nilsen, T. Purdin, and G. Townsend.: An Overview of the SR Language and Implementation. ACM Transactions on Programming Languages and Systems 10, 1 (January 1988), 51\u201386.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR2","volume-title":"Concurrent Programming: Principles and Practice","author":"G.R. Andrews","year":"1991","unstructured":"G.R. Andrews.: Concurrent Programming: Principles and Practice. The Benjamin\/Cummings Publishing Company, Inc. Redwood City, CA, 1991."},{"key":"3_CR3","volume-title":"The SR Programming Language: Concurrency in Practice","author":"G.R. Andrews","year":"1993","unstructured":"G.R. Andrews and R.A. Olsson.: The SR Programming Language: Concurrency in Practice. Benjamin\/Cummings Publishing Company, Inc. Redwood City, CA, 1993."},{"key":"3_CR4","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"W.R. Bevier, W.A. Hunt, J.S. Moore, and W.D. Young.: An approach to systems verification. Journal of Automated Reasoning, 5:411\u2013428, 1989.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"M. Chandy and J. Misra.: Parallel Program Design: A Foundation of Programming Logic. Addison-Wesley Publishing Company, Inc. 1988.","key":"3_CR5"},{"key":"3_CR6","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M. J. C. Gordon","year":"1989","unstructured":"M. J. C. Gordon.: Mechanizing Programming Logics in Higher Order Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, New York, 1989."},{"key":"3_CR7","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"W. Harrison","year":"1993","unstructured":"W. Harrison, K. Levitt, and M. Archer.: A HOL Mechanization of the Axiomatic Semantics of a Simple Distributed Programming Language. In: Higher Order Logic Theorem Proving and Its Applications. North-Holland, Netherlands, 1993."},{"key":"3_CR8","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, N.J., 1985."},{"unstructured":"J.J. Joyce.: A Verified Compiler for a Verified Microprocessor. Technical Report No. 167, Computer Laboratory, University of Cambridge, March 1989.","key":"3_CR9"},{"key":"3_CR10","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and Computation: Interactive Proof with Cambridge LCF","author":"L. C. Paulson","year":"1987","unstructured":"L. C. Paulson.: Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge; New York: Cambridge University Press, 1987."},{"key":"3_CR11","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W. D. Young","year":"1989","unstructured":"W. D. Young.: A Mechanically Verified Code Generator. Journal of Automated Reasoning, Vol. 5: 493\u2013518, 1989.","journal-title":"Journal of Automated Reasoning"}],"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-57826-9_123.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:08:26Z","timestamp":1619572106000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_123","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}