{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:52Z","timestamp":1725467512324},"publisher-location":"Berlin, Heidelberg","reference-count":11,"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\/bfb0055128","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"33-48","source":"Crossref","is-referenced-by-count":1,"title":["Program abstraction in a higher-order logic framework"],"prefix":"10.1007","author":[{"given":"Marco","family":"Benini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sara","family":"Kalvala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Nowotka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"3_CR2","unstructured":"Michael J. C. Gordon and Tom F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"3_CR3","unstructured":"Robin Milner. An algebraic definition of simulation between programs. In Second Joint Conference on Artificial Intelligence, pages 481\u2013489, 1971."},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"3_CR5","volume-title":"International Series in Computer Science","author":"R. Milner","year":"1989","unstructured":"Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, London, 1989."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"3_CR7","unstructured":"Lawrence C. Paulson. A fixedpoint approach to (co)inductive and (co)datatype definitions. Technical Report 304, Computer Laboratory, University of Cambridge, May 1997."},{"key":"3_CR8","unstructured":"Lawrence C. Paulson. Isabelle's object-logics. Technical Report 286, Computer Laboratory, University of Cambridge, May 1997."},{"issue":"7","key":"3_CR9","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1093\/comjnl\/36.7.654","volume":"36","author":"D. Pavey","year":"1993","unstructured":"D. Pavey and L. Winsborrow. Demonstrating equivalence of source code and PROM contents. The Computer Journal, 36(7):654\u2013667, 1993.","journal-title":"The Computer Journal"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/0890-5401(90)90048-M","volume":"85","author":"D. Walker","year":"1990","unstructured":"David Walker. Bisimulation and divergence. Information and Computation, 85:202\u2013241, 1990.","journal-title":"Information and Computation"},{"key":"3_CR11","volume-title":"Research Report 114","author":"Y. Yu","year":"1993","unstructured":"Yuan Yu. Automated proofs of object code for a widely used microprocessor. Research Report 114, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, October 1993."}],"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\/BFb0055128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T08:34:14Z","timestamp":1555749254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0055128","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}