Abstract
In this entry we formalize Isabelle's metalogic in Isabelle/HOL.
Furthermore, we define a language of proof terms and an executable
proof checker and prove its soundness wrt. the metalogic. The
formalization is intentionally kept close to the Isabelle
implementation(for example using de Brujin indices) to enable easy
integration of generated code with the Isabelle system without a
complicated translation layer. The formalization is described in our
CADE 28 paper.
License
Topics
Related publications
- Nipkow, T., & Roßkopf, S. (2021). Isabelle’s Metalogic: Formalization and Proof Checker. Lecture Notes in Computer Science, 93–110. https://doi.org/10.1007/978-3-030-79876-5_6
- Roßkopf, S., & Nipkow, T. (2022). A Formalization and Proof Checker for Isabelle’s Metalogic. Journal of Automated Reasoning, 67(1). https://doi.org/10.1007/s10817-022-09648-w
Session Metalogic_ProofChecker
- Core
- Preliminaries
- Term
- Sorts
- SortConstants
- Theory
- Term_Subst
- Name
- BetaNorm
- BetaNormProof
- EtaNorm
- EtaNormProof
- Logic
- EqualityProof
- ProofTerm
- SortsExe
- Instances
- TheoryExe
- CheckerExe
- CodeGen