{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:47:12Z","timestamp":1748072832289},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_28","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:51:33Z","timestamp":1330249893000},"page":"288-298","source":"Crossref","is-referenced-by-count":7,"title":["Mechanizing a proof by induction of process algebra specifications in higher order logic"],"prefix":"10.1007","author":[{"given":"Monica","family":"Nesi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Camilleri A. J., \u2018Mechanizing CSP Trace Theory in Higher Order Logic', IEEE Transactions on Software Engineering, Special Issue on Formal Methods, N. G. Leveson (ed.), September 1990, Vol. 16, No. 9, pp. 993\u20131004.","DOI":"10.1109\/32.58786"},{"key":"28_CR2","volume-title":"Proc. of the 4th Banff Higher Order Workshop","author":"A. J. Camilleri","year":"1991","unstructured":"Camilleri A. J., \u2018A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics', Proc. of the 4th Banff Higher Order Workshop, G. Birtwistle (ed.), Springer-Verlag, London, 1991, (to appear)."},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Camilleri A. J., Inverardi P., Nesi M., \u2018Combining Interaction and Automation in Process Algebra Verification', Proc. of TAPSOFT '91, Lecture Notes in Computer Science, Springer-Verlag, 1991, Vol. 494, pp. 283\u2013296.","DOI":"10.1007\/3540539816_72"},{"issue":"No.2","key":"28_CR4","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF01383954","volume":"12","author":"R. Cleaveland","year":"1988","unstructured":"Cleaveland R., Panangaden P., \u2018Type Theory and Concurrency', International Journal of Parallel Programming, November 1988, Vol. 12, No. 2, pp. 153\u2013206.","journal-title":"International Journal of Parallel Programming"},{"key":"28_CR5","unstructured":"Cousineau G., Huet G., Paulson L., \u2018The ml Handbook', INRIA, 1986."},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"De Nicola R., Inverardi P., Nesi M., \u2018Using the Axiomatic Presentation of Behavioural Equivalences for Manipulating CCS Specifications', Proc. of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, Springer-Verlag, 1990, Vol. 407, pp. 54\u201367.","DOI":"10.1007\/3-540-52148-8_5"},{"key":"28_CR7","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. J. C. C. Gordon","year":"1988","unstructured":"Gordon M. J. C., \u2018HOL\u2014A Proof Generating System for Higher-Order Logic', VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam (eds.), Kluwer Academic Publishers, Boston, 1988, pp. 73\u2013128."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Gordon M. J. C., \u2018Mechanizing Programming Logics in Higher Order Logic', Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle and P. Subrahmanyam (eds.), Springer-Verlag, 1989, pp. 387\u2013439.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"28_CR9","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/0020-0190(90)90023-Q","volume":"35","author":"P. Inverardi","year":"1990","unstructured":"Inverardi P., Nesi M., \u2018A Rewriting Strategy to Verify Observational Congruence', Information Processing Letters, 1990, Vol. 35, pp. 191\u2013199.","journal-title":"Information Processing Letters"},{"key":"28_CR10","unstructured":"Lin H., \u2018PAM: A Process Algebra Manipulator', this volume."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Melham T. F., \u2018Automating Recursive Type Definitions in Higher Order Logic', Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle and P. Subrahmanyam (eds.), Springer-Verlag, 1989, pp. 341\u2013386.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"28_CR12","unstructured":"Melham T. F., \u2018A Mechanized Theory of the \u03c0-calculus in hol', Proc. of the 2nd Annual Esprit BRA Workshop on Logical Frameworks, Univ. of Edinburgh, 1991."},{"key":"28_CR13","unstructured":"Milner R., Communication and Concurrency, Prentice Hall, 1989."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Paulson L. C., Logic and Computation\u2014Interactive Proof with Cambridge lcf, Cambridge Tracts in Theoretical Computer Science (2), Cambridge Univ. Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"28_CR15","unstructured":"Proc. of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, Springer-Verlag, 1990, Vol. 407."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:57:57Z","timestamp":1605646677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}