{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:54:41Z","timestamp":1742388881655},"publisher-location":"Berlin, Heidelberg","reference-count":9,"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\/bfb0055134","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"143-152","source":"Crossref","is-referenced-by-count":4,"title":["Adding external decision procedures to HOL90 securely"],"prefix":"10.1007","author":[{"given":"Elsa L.","family":"Gunter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"R. J. Boulton. A Lazy Approach to Fully-Expansive Theorem Proving. In Higher Order Logic Theorem Proving and Its Applications. North-Holland, 1992.","DOI":"10.1016\/B978-0-444-89880-7.50008-5"},{"key":"9_CR2","unstructured":"M. J. C. Gordon and T. Melham, Introduction to HOL. Cambridge University Press, 1993."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL theorem prover with a Computer Algebra System to Reason about the Reals. In Higher Order Logic Theorem Proving and Its Applications. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_134"},{"issue":"No.2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P. V. Homeier","year":"1995","unstructured":"P. V. Homeier and D. F. Martin. A Mechanically Verified Verification Condition Generator. In The Computer Journal, Vol. 38, No. 2, July 1995, pages 131\u2013141.","journal-title":"The Computer Journal"},{"key":"9_CR5","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall Software Series, 1991."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In Proceedings of CAV'96, Lecture Notes in Computer Science. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_91"},{"key":"9_CR8","unstructured":"L. C. Paulson. The Isabelle Reference Manual. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/dist\/Isabelle98\/doc\/ref.dvi"},{"key":"9_CR9","unstructured":"K. Schneider, R. Kuma, and T. Kropf. Integrating a first-order automatic prover in the HOL environment. In Proceedings of the 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications. IEEE Computer Society Press, 1992."}],"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\/BFb0055134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:33:57Z","timestamp":1555734837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/bfb0055134","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}