{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:28Z","timestamp":1742617168358,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601173"},{"type":"electronic","value":"9783540494454"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60117-1_17","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:43:29Z","timestamp":1330278209000},"page":"304-321","source":"Crossref","is-referenced-by-count":2,"title":["Algebraic proof assistants in HOL"],"prefix":"10.1007","author":[{"given":"Rix","family":"Groenboom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Hendriks","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Indra","family":"Polak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Terlouw","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan Tijmen","family":"Udding","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"17_CR1","unstructured":"M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report 88, Logic Group Preprint Series, Utrecht University, March 1993."},{"key":"17_CR2","unstructured":"G. Birtwistle and B. Graham. Verifying SECD in HOL. In Proceedings of the IFIP TC10\/WG10.5 Summer School on Formal Methods for VLSI Design, North Holland, 1990."},{"key":"17_CR3","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"A.J. Camilleri. A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics. In Proceedings of the 4th Banff Higher Order Workshop, G. Birtwistle (ed.), Workshops in Computing Series, Springer Verlag, 1991, pp. 123\u2013150.","DOI":"10.1007\/978-1-4471-3182-3_9"},{"key":"17_CR5","unstructured":"M.J.C. Gordon en T.F. Melham. Introduction to HOL. Cambridge University Press, 1993."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"M. Heisel, W. Reif and W. Stephan, Tactical Theorem Proving in Program Verification, In: Conference on Automated Deduction, Siekmann (ed), LNCS 449, Spinger Verlag, 1990, pp. 117\u2013131.","DOI":"10.1007\/3-540-52885-7_83"},{"issue":"Nr4","key":"17_CR7","first-page":"429","volume":"5","author":"W. A. Hunt Jr","year":"1989","unstructured":"Warren A. Hunt, Jr, Microprocessor Design Verification. Journal of Automated Reasoning, Vol 5, Nr 4, December 1989, pp. 429\u2013460.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"M.B. Josephs and J.T. Udding, An Overview of DI Algebra. In: Proc. Hawaii International Conf. System Sciences, T.N. Mudge and V. Milutinovic and L. Hunter (eds), Vol. I, IEEE Computer Society Press, 1993, pp. 329\u2013338.","DOI":"10.1109\/HICSS.1993.270632"},{"key":"17_CR9","volume-title":"PhD thesis","author":"P. G. Lucassen","year":"1994","unstructured":"P. G. Lucassen. A Denotational Model and Composition Theorems for a Calculus of Delay-Insensitive Specifications. PhD thesis, Dept. of C.S., Univ. of Groningen, The Netherlands, May 1994."},{"key":"17_CR10","unstructured":"M. Nesi. A Formalization of the Process Algebra CCS in Higher Order Logic. Technical Report 278, University of Cambrigde Computer Laboratory, December 1992."},{"key":"17_CR11","first-page":"315","volume-title":"Verifying Process Algebra Proofs in Type Theory","author":"M.P.A. Sellink","year":"1994","unstructured":"M.P.A. Sellink. Verifying Process Algebra Proofs in Type Theory, In: Proceedings of Workshop in Semantics of Specification Languages, D.J. Andrews, J.F. Groote and C.A. Middelburg (eds), October 1993, Utrecht, Springer Verlag, 1994, pp. 315\u2013339."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60117-1_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:52:56Z","timestamp":1742597576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60117-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601173","9783540494454"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-60117-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}