{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:37Z","timestamp":1761611077536,"version":"3.43.0"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,3,1]],"date-time":"1999-03-01T00:00:00Z","timestamp":920246400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1999,3]]},"DOI":"10.1023\/a:1008643803725","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"193-212","source":"Crossref","is-referenced-by-count":9,"title":["Validation of HOL Proofs by Proof Checking"],"prefix":"10.1007","volume":"14","author":[{"given":"Wai","family":"Wong","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"200090_CR1","unstructured":"R.J. Boulton, \u201cOn efficiency in theorem provers which fully expand proofs into primitive inferences,\u201d Technical Report 248, University of Cambridge Computer Laboratory, 1992."},{"key":"200090_CR2","unstructured":"Robert S. Boyer and Gilles Dowek, \u201cTowards checking proof checkers,\u201d in Workshop on Types for Proofs and Programs (Type '93), 1993."},{"issue":"2","key":"200090_CR3","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF00243000","volume":"5","author":"A. Cohn","year":"1989","unstructured":"A. Cohn, \u201cThe notion of proof in hardware verification,\u201d Journal of Automated Reasoning, Vol. 5,No. 2, pp. 127\u2013139, June 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"200090_CR4","unstructured":"Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1996."},{"issue":"9","key":"200090_CR5","doi-asserted-by":"crossref","first-page":"1048","DOI":"10.1145\/48529.48530","volume":"31","author":"J. H. Fetzer","year":"1988","unstructured":"James H. Fetzer, \u201cProgram verification: the very idea,\u201d Communications of the ACM, Vol. 31,No. 9, pp. 1048\u20131063, Sept. 1988.","journal-title":"Communications of the ACM"},{"key":"200090_CR6","unstructured":"M.J.C. Gordon, \u201cLCF_LSM, A system for specifying and verifying hardware,\u201d Technical Report 41, University of Cambridge Computer Laboratory, 1983."},{"key":"200090_CR7","unstructured":"M.J.C. Gordon and T.F. Melham (Eds.), Introduction to HOL-A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"200090_CR8","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science No. 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"200090_CR9","unstructured":"Ministry of Defence, Requirements for the Procurement of Safety-Critical Software in Defence Equipment, Interim Standard 00\u201355, April 1991."},{"issue":"2","key":"200090_CR10","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1109\/2.566148","volume":"30","author":"S. L. Pfleeger","year":"1997","unstructured":"Shari L. Pfleeger and Les Hatton, \u201cInvestigating the influence of formal methods,\u201d IEEE Computer, Vol. 30,No. 2, pp. 33\u201343, Feb. 1997.","journal-title":"IEEE Computer"},{"key":"200090_CR11","doi-asserted-by":"crossref","unstructured":"D. Syme, \u201cReasoning with the formal definition of standard ML in HOL,\u201d Higher Order Logic Theorem Proving and its Applications, Lecture Notes in Computer Science No. 780, Springer-Verlag, 1993, pp. 43\u201358.","DOI":"10.1007\/3-540-57826-9_124"},{"key":"200090_CR12","unstructured":"M. VanInwegen and E. Gunter, \u201cHOL-ML,\u201d Higher Order Logic Theorem Proving and its Applications, Lecture Notes in Computer Science No. 780, Springer-Verlag, 1993, pp. 59\u201372."},{"key":"200090_CR13","doi-asserted-by":"crossref","unstructured":"J. von Wright, \u201cRepresenting higher-order logic proofs in HOL,\u201d Technical Report 323, University of Cambridge Computer Laboratory, Jan. 1994.","DOI":"10.1007\/3-540-58450-1_60"},{"key":"200090_CR14","doi-asserted-by":"crossref","unstructured":"J. von Wright, \u201cProgram refinement by theorem prover,\u201d in Proceedings of the 6th Refinement Workshop, Lecture Notes in Computer Science, Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4471-3240-0_7"},{"key":"200090_CR15","series-title":"Technical Report","volume-title":"Recording HOL proofs","author":"W. Wong","year":"1993","unstructured":"W. Wong, \u201cRecording HOL proofs,\u201d Technical Report 306, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, July 1993."},{"key":"200090_CR16","unstructured":"W. Wong, The HOL record-proof Library: A HOL system library manual, Computer Laboratory, University of Cambridge, 1994."},{"key":"200090_CR17","series-title":"Technical Report","volume-title":"A proof checker for HOL proofs","author":"W. Wong","year":"1995","unstructured":"W. Wong, \u201cA proof checker for HOL proofs,\u201d Technical Report 389, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, 1995."},{"key":"200090_CR18","unstructured":"W. Wong and P. Curzon, \u201cTowards an efficient proof recorder for HOL90,\u201d in Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logic:TPHOL '97, 1997."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008643803725.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008643803725\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008643803725.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:14:26Z","timestamp":1754367266000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008643803725"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,3]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,3]]}},"alternative-id":["200090"],"URL":"https:\/\/doi.org\/10.1023\/a:1008643803725","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1999,3]]}}}