{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:49:16Z","timestamp":1766137756147,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle\/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_6","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"93-110","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Isabelle\u2019s Metalogic: Formalization and Proof Checker"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7955-8749","authenticated-orcid":false,"given":"Simon","family":"Ro\u00dfkopf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"\u00c5man Pohjola, J., Gengelbach, A.: A mechanised semantics for HOL with ad-hoc overloading. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 498\u2013515. EasyChair (2020), https:\/\/doi.org\/10.29007\/413d","DOI":"10.29007\/413d"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Abrahamsson, O.: A verified proof checker for higher-order logic. J. Log. Algebraic Methods Program. 112, 100530 (2020), https:\/\/doi.org\/10.1016\/j.jlamp.2020.100530","DOI":"10.1016\/j.jlamp.2020.100530"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Adams, M.: HOL Zero\u2019s solutions for Pollack-inconsistency. Lect. Notes in Comp. Sci., vol.\u00a09807, pp. 20\u201335. Springer (2016), https:\/\/doi.org\/10.1007\/978-3-319-43144-4_2","DOI":"10.1007\/978-3-319-43144-4_2"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Harrison, J., Aagaard, M. (eds.) Theorem Proving in Higher Order Logics. Lect. Notes in Comp. Sci., vol.\u00a01869, pp. 38\u201352. Springer (2000)","DOI":"10.1007\/3-540-44659-1_3"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Types for Proofs and Programs (TYPES 2000). Lect. Notes in Comp. Sci., vol.\u00a02277, pp. 24\u201340. Springer (2002)","DOI":"10.1007\/3-540-45842-5_2"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Carneiro, M.M.: Metamath Zero: Designing a theorem prover prover. In: Benzm\u00fcller, C., Miller, B.R. (eds.) Intelligent Computer Mathematics, CICM 2020. Lect. Notes in Comp. Sci., vol. 12236, pp. 71\u201388. Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-53518-6_5","DOI":"10.1007\/978-3-030-53518-6_5"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Gheri, L., Popescu, A.: A formalized general theory of syntax with bindings: Extended version. J. Automated Reasoning 64(4), 641\u2013675 (2020), https:\/\/doi.org\/10.1007\/s10817-019-09522-2","DOI":"10.1007\/s10817-019-09522-2"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP 2013). Lect. Notes in Comp. Sci., vol.\u00a07998, pp. 100\u2013115. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming (FLOPS 2010). Lect. Notes in Comp. Sci., vol.\u00a06009, pp. 103\u2013117. Springer (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, TYPES 2006. Lect. Notes in Comp. Sci., vol.\u00a04502, pp. 160\u2013174. Springer (2006), https:\/\/doi.org\/10.1007\/978-3-540-74464-1_11","DOI":"10.1007\/978-3-540-74464-1_11"},{"key":"6_CR11","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) Proceedings of the third International Joint Conference, IJCAR 2006. Lect. Notes in Comp. Sci., vol.\u00a04130, pp. 177\u2013191. Springer, Seattle, WA (2006)"},{"key":"6_CR12","unstructured":"Hurd, J.: OpenTheory: Package management for higher order logic theories. In: Reis, G., Th\u00e9ry, L. (eds.) Workshop on Programming Languages for Mechanized Mathematics Systems (ACM SIGSAM PLMMS 2009). pp. 31\u201337 (2009)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higher-order logic \u2014 semantics, soundness, and a verified implementation. J. Automated Reasoning 56(3), 221\u2013259 (2016), https:\/\/doi.org\/10.1007\/s10817-015-9357-x","DOI":"10.1007\/s10817-015-9357-x"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Principles of Programming Languages (POPL). pp. 179\u2013191. ACM Press (Jan 2014), https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2578855.2535841"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O., Popescu, A.: A consistent foundation for Isabelle\/HOL. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving, ITP 2015. Lect. Notes in Comp. Sci., vol.\u00a09236, pp. 234\u2013252. Springer (2015), https:\/\/doi.org\/10.1007\/978-3-319-22102-1_16","DOI":"10.1007\/978-3-319-22102-1_16"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O., Popescu, A.: Comprehending Isabelle\/HOL\u2019s consistency. In: Yang, H. (ed.) Programming Languages and Systems, ESOP 2017. Lect. Notes in Comp. Sci., vol. 10201, pp. 724\u2013749. Springer (2017), https:\/\/doi.org\/10.1007\/978-3-662-54434-1_27","DOI":"10.1007\/978-3-662-54434-1_27"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O., Popescu, A.: Safety and conservativity of definitions in HOL and Isabelle\/HOL. Proc. ACM Program. Lang. 2(POPL), 24:1\u201324:26 (2018), https:\/\/doi.org\/10.1145\/3158112","DOI":"10.1145\/3158112"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O., Popescu, A.: A consistent foundation for Isabelle\/HOL. J. Automated Reasoning 62(4), 531\u2013555 (2019), https:\/\/doi.org\/10.1007\/s10817-018-9454-8","DOI":"10.1007\/s10817-018-9454-8"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, ITP 2010. Lect. Notes in Comp. Sci., vol.\u00a06172, pp. 339\u2013354. Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-14052-5_24","DOI":"10.1007\/978-3-642-14052-5_24"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Light-weight containers for isabelle: Efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, ITP 2013. Lect. Notes in Comp. Sci., vol.\u00a07998, pp. 116\u2013132. Springer (2013), https:\/\/doi.org\/10.1007\/978-3-642-39634-2_11","DOI":"10.1007\/978-3-642-39634-2_11"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Journal of Automated Reasonig: Special Issue: Theory and Applications of Abstraction, Substitution and Naming, vol. 49. Springer (Aug 2012), https:\/\/link.springer.com\/journal\/10817\/volumes-and-issues\/49-2","DOI":"10.1007\/s10817-011-9217-2"},{"key":"6_CR22","unstructured":"Nipkow, T.: Order-sorted polymorphism in Isabelle. In: Huet, G., Plotkin, G. (eds.) Logical Environments. pp. 164\u2013188. Cambridge University Press (1993)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: More Church-Rosser proofs (in Isabelle\/HOL). J. Automated Reasoning 26, 51\u201366 (2001)","DOI":"10.1023\/A:1006496715975"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer (2014), http:\/\/concrete-semantics.org","DOI":"10.1007\/978-3-319-10542-0"},{"key":"6_CR25","doi-asserted-by":"publisher","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","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, D. (ed.) Automated Deduction - CADE-11. Lect. Notes in Comp. Sci., vol. 607, pp. 673\u2013676. Springer (1992), https:\/\/doi.org\/10.1007\/3-540-55602-8_201","DOI":"10.1007\/3-540-55602-8_201"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Prehofer, C.: Type reconstruction for type classes. J. Functional Programming 5(2), 201\u2013224 (1995)","DOI":"10.1017\/S0956796800001325"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Ro\u00dfkopf, S.: Isabelle\u2019s metalogic: Formalization and proof checker. Archive of Formal Proofs (Apr 2021), https:\/\/isa-afp.org\/entries\/Metalogic_ProofChecker.html, Formal proof development","DOI":"10.1007\/s10817-022-09648-w"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Snelting, G.: Type classes and overloading resolution via order-sorted unification. In: Hughes, J. (ed.) Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture. Lect. Notes in Comp. Sci., vol.\u00a0523, pp. 1\u201314. Springer (1991)","DOI":"10.1007\/3540543961_1"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Automated Reasoning 5, 363\u2013397 (1989)","DOI":"10.1007\/BF00248324"},{"key":"6_CR31","doi-asserted-by":"publisher","unstructured":"Paulson, L.C. (ed.): Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541","DOI":"10.1007\/BFb0030541"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Pelletier, F.: Seventy-five problems for testing automatic theorem provers. J. Automated Reasoning 2, 191\u2013216 (06 1986), https:\/\/doi.org\/10.1007\/BF02432151","DOI":"10.1007\/BF02432151"},{"key":"6_CR33","unstructured":"Pfenning, F.: Elf: A language for logic definition and verified metaprogramming. In: Logic in Computer Science (LICS 1989). pp. 313\u2013322. IEEE Computer Society Press (1989)"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction, CADE-16. Lect. Notes in Comp. Sci., vol. 1632, pp. 202\u2013206. Springer (1999), https:\/\/doi.org\/10.1007\/3-540-48660-7_14","DOI":"10.1007\/3-540-48660-7_14"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Pientka, B.: Beluga: Programming with dependent types, contextual data, and contexts. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, FLOPS 2010. Lect. Notes in Comp. Sci., vol.\u00a06009, pp. 1\u201312. Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-12251-4_1","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4(POPL), 8:1\u20138:28 (2020), https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J. Automated Reasoning 40, 327\u2013356 (2008), https:\/\/doi.org\/10.1007\/s10817-008-9097-2","DOI":"10.1007\/s10817-008-9097-2"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) Theorem Proving in Higher Order Logics, TPHOLs\u201997. Lect. Notes in Comp. Sci., vol.\u00a01275, pp. 307\u2013322. Springer (1997), https:\/\/doi.org\/10.1007\/BFb0028402","DOI":"10.1007\/BFb0028402"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:24:46Z","timestamp":1672723486000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"5","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":"2 invited papers and 7 system descriptions are also included.","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)"}}]}}