@inproceedings{587a2dbe1c7e4267af3f6de8a8be5429,
title = "Isabelle{\textquoteright}s Metalogic: Formalization and Proof Checker",
abstract = "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.",
author = "Tobias Nipkow and Simon Ro{\ss}kopf",
note = "Publisher Copyright: {\textcopyright} 2021, The Author(s).; 28th International Conference on Automated Deduction, CADE 28 2021 ; Conference date: 12-07-2021 Through 15-07-2021",
year = "2021",
doi = "10.1007/978-3-030-79876-5_6",
language = "English",
isbn = "9783030798758",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "93--110",
editor = "Andr{\'e} Platzer and Geoff Sutcliffe",
booktitle = "Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings",
}