{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:44:27Z","timestamp":1766137467336,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030535179"},{"type":"electronic","value":"9783030535186"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_5","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"71-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Metamath Zero: Designing a Theorem Prover Prover"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0470-5249","authenticated-orcid":false,"given":"Mario","family":"Carneiro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Armstrong, A., et al.: ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In: Proceedings of 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. https:\/\/doi.org\/10.1145\/3290384. Proc. ACM Program. Lang. 3(POPL), Article 71","DOI":"10.1145\/3290384"},{"key":"5_CR2","unstructured":"Barras, B.: Coq en coq (1996)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 38\u201352. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_3"},{"issue":"1\u20134","key":"5_CR4","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-FLOYD: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1\u20134), 367\u2013422 (2018)","journal-title":"J. Autom. Reason."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Carneiro, M.: Metamath Zero: The Cartesian Theorem Prover (2019, preprint)","DOI":"10.1007\/978-3-030-53518-6_5"},{"key":"5_CR6","unstructured":"Carneiro, M.: Specifying verified x86 software from scratch. In: Workshop on Instruction Set Architecture Specification (SpISA 2019) (2019). https:\/\/www.cl.cam.ac.uk\/~jrh13\/spisa19\/paper_07.pdf"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Ro\u015fu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019), pp. 1133\u20131148. ACM, June 2019. https:\/\/doi.org\/10.1145\/3314221.3314601","DOI":"10.1145\/3314221.3314601"},{"key":"5_CR8","unstructured":"Davis, J.C., Moore, J.S.: A self-verifying theorem prover. Ph.D. thesis, University of Texas (2009)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Goel, S., Slobodova, A., Sumners, R., Swords, S.: Verifying x86 instruction implementations. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 47\u201360 (2020)","DOI":"10.1145\/3372885.3373811"},{"key":"5_CR10","unstructured":"Haftmann, F.: Code generation from Isabelle\/HOL theories"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/11814771_17","volume-title":"Automated Reasoning","author":"J Harrison","year":"2006","unstructured":"Harrison, J.: Towards self-verification of HOL light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 177\u2013191. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_17"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL), 1\u201334 (2017)","DOI":"10.1145\/3158154"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-319-94821-8_21","volume-title":"Interactive Theorem Proving","author":"R Kumar","year":"2018","unstructured":"Kumar, R., Mullen, E., Tatlock, Z., Myreen, M.O.: Software verification with ITPs should use binary code extraction to reduce the TCB. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 362\u2013369. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_21"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. SIGPLAN Not. 49(1), 179\u2013191 (2014). https:\/\/doi.org\/10.1145\/2578855.2535841","DOI":"10.1145\/2578855.2535841"},{"key":"5_CR16","unstructured":"Leroy, X., et al.: The compcert verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt 53 (2012)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69407-6_39"},{"key":"5_CR18","volume-title":"Metamath: A Computer Language for Mathematical Proofs","author":"N Megill","year":"2019","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville (2019)"},{"key":"5_CR19","unstructured":"Myreen, M.O.: Formal verification of machine-code programs. Technical report, University of Cambridge, Computer Laboratory (2009)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-22863-6_20","volume-title":"Interactive Theorem Proving","author":"MO Myreen","year":"2011","unstructured":"Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 265\u2013280. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_20"},{"issue":"6","key":"5_CR21","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/j.jlap.2010.03.012","journal-title":"J. Logic Algebraic Program."},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-030-23250-4_17","volume-title":"Intelligent Computer Mathematics","author":"C Sacerdoti Coen","year":"2019","unstructured":"Sacerdoti Coen, C.: A plugin to export Coq libraries to XML. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 243\u2013257. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_17"},{"key":"5_CR23","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":"5_CR24","unstructured":"Sozeau, M., Forster, Y., Winterhalter, T.: Coq Coq correct!"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T23:16:30Z","timestamp":1619219790000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}