{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:27:18Z","timestamp":1783348038811,"version":"3.54.6"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032306920","type":"print"},{"value":"9783032306937","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:00:00Z","timestamp":1782950400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2027]]},"DOI":"10.1007\/978-3-032-30693-7_8","type":"book-chapter","created":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:10:28Z","timestamp":1783347028000},"page":"121-139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A HOL Theorem Proving Interface for\u00a0C"],"prefix":"10.1007","author":[{"given":"Yiyuan","family":"Cao","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiayi","family":"Zhuang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jinkai","family":"Fan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Di","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,2]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Adams, M.: The common HOL platform. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. EPTCS, vol.\u00a0186, pp. 42\u201356 (2015). https:\/\/doi.org\/10.4204\/EPTCS.186.6","DOI":"10.4204\/EPTCS.186.6"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 7:1\u20137:31 (2015). https:\/\/doi.org\/10.1145\/2701415","DOI":"10.1145\/2701415"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Boehm, H.J.: Space efficient conservative garbage collection. In: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation. PLDI 1993 pp. 197\u2013206. ACM, Albuquerque New Mexico (1993). https:\/\/doi.org\/10.1145\/155090.155109","DOI":"10.1145\/155090.155109"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Cao, Y., Zhuang, J., Fan, J., Wang, D., Hu, Z.: Artifact for \u201cA HOL Theorem Proving Interface for C\u201d (2026). https:\/\/doi.org\/10.5281\/zenodo.18887462","DOI":"10.5281\/zenodo.18887462"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Gordon, M.J.C., Milner, R., Morris, F.L., Newey, M.C., Wadsworth, C.P.: A metalanguage for interactive proof in LCF. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 119\u2013130. ACM Press, Tucson, Arizona, USA (1978). https:\/\/doi.org\/10.1145\/512760.512773","DOI":"10.1145\/512760.512773"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Gordon, M.: From LCF to HOL: a short history. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 169\u2013186. The MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0012"},{"key":"8_CR9","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Keeton, K., Roscoe, T. (eds.) 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, pp. 653\u2013669. USENIX Association (2016). https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"issue":"11","key":"8_CR10","first-page":"1370","volume":"55","author":"TC Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Notices AMS 55(11), 1370\u20131380 (2008)","journal-title":"Notices AMS"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Matthews, J.N., Anderson, T.E. (eds.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pp. 207\u2013220. ACM (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20-21, 2014, pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"8_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Martin-L\u00f6f, P., Cohen, L.J., \u0141o\u015b, J., Pfeiffer, H.: Constructive mathematics and computer programming. In: Podewski, K.P. (ed.) Logic, Methodology and Philosophy of Science VI, Studies in Logic and the Foundations of Mathematics, vol. 104, pp. 153\u2013175. Elsevier (1982). https:\/\/doi.org\/10.1016\/S0049-237X(09)70189-2","DOI":"10.1016\/S0049-237X(09)70189-2"},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/S10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T.C., Wenzel, M.: Eisbach: a proof method language for isabelle. J. Autom. Reason. 56(3), 261\u2013282 (2016). https:\/\/doi.org\/10.1007\/S10817-015-9360-2","journal-title":"J. Autom. Reason."},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Milner, R.: The use of machines to assist in rigorous proof. Philos. Trans. R. Soc. London, Series A: Math. Phys. Sci. 312(1522), 411\u2013422 (1984). https:\/\/doi.org\/10.1098\/rsta.1984.0067","DOI":"10.1098\/rsta.1984.0067"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Mulligan, D.P.: All watched over by machines of loving grace. In: Kesner, D., P\u00e9drot, P. (eds.) 28th International Conference on Types for Proofs and Programs, TYPES 2022, LS2N, University of Nantes, France, June 20-25, 2022. LIPIcs, vol.\u00a0269, pp. 1:1\u20131:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.TYPES.2022.1,","DOI":"10.4230\/LIPICS.TYPES.2022.1"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"LC Paulson","year":"1983","unstructured":"Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119\u2013149 (1983). https:\/\/doi.org\/10.1016\/0167-6423(83)90008-4","journal-title":"Sci. Comput. Program."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Logic and computation - interactive proof with Cambridge LCF, Cambridge tracts in theoretical computer science, vol. 2, Cambridge University Press, Cambridge (1987)","DOI":"10.1017\/CBO9780511526602"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) Proceedings of the ACM SIGPLAN\u201988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, pp. 199\u2013208. ACM (1988). https:\/\/doi.org\/10.1145\/53990.54010,","DOI":"10.1145\/53990.54010"},{"key":"8_CR25","unstructured":"Pitts, A.M.: The HOL System: Logic, Trindemossen-2 Edition (2025). https:\/\/github.com\/HOL-Theorem-Prover\/HOL\/releases\/download\/trindemossen-2\/trindemossen-2-logic.pdf"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"8_CR27","unstructured":"Varda, K.: Cap\u2019n proto. https:\/\/capnproto.org\/"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_12"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Thuraisingham, B., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pp. 1789\u20131806. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-30693-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,6]],"date-time":"2026-07-06T14:10:42Z","timestamp":1783347042000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-30693-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7,2]]},"ISBN":["9783032306920","9783032306937"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-30693-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,7,2]]},"assertion":[{"value":"2 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Shanghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2026.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}