Isabelle's Metalogic: Formalization and Proof Checker
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.
arXiv
BibTeX:
@inproceedings{NipkowRosskopf-CADE21,author={Tobias Nipkow and Simon Ro{\ss}kopf},
title={Isabelle's Metalogic: Formalization and Proof Checker},
booktitle="Automated Deduction --- CADE-28",editor={A. Platzer and G. Sutcliff},
year=2021,publisher={Springer},series={LNCS},volume={12699},pages={93--110}}
Springer's final version
Isabelle formalization