A formalization and proof checker for Isabelle's metalogic

DOI10.1007/s10817-022-09648-wzbMath1502.68353OpenAlexW4312126060MaRDI QIDQ2108191

Simon Roßkopf, Tobias Nipkow

Publication date: 19 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09648-w

zbMATH Keywords

theorem provinghigher-order logicIsabellemetalogicproof checker

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Twelf
• CakeML
• Milawa
• Nominal Isabelle
• Jitawa
• HOL Zero
• Transfer
• Lifting
• Elf
• OpenTheory
• Metamath Zero

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Nominal techniques in Isabelle/HOL
• Seventy-five problems for testing automatic theorem provers
• Isabelle. A generic theorem prover
• More Church-Rosser proofs (in Isabelle/HOL)
• Isabelle/HOL. A proof assistant for higher-order logic
• A consistent foundation for Isabelle/HOL
• The foundation of a generic theorem prover
• A formalized general theory of syntax with bindings: extended version
• A verified proof checker for higher-order logic
• Isabelle's metalogic: formalization and proof checker
• Metamath Zero: designing a theorem prover prover
• HOL Zero’s Solutions for Pollack-Inconsistency
• Concrete Semantics
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Consistent Foundation for Isabelle/HOL
• Comprehending Isabelle/HOL’s Consistency
• Code Generation via Higher-Order Rewrite Systems
• Constructive Type Classes in Isabelle
• Towards Self-verification of HOL Light
• Type Reconstruction for Type Classes
• Data Refinement in Isabelle/HOL
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• CakeML
• The Isabelle Collections Framework

This page was built for publication: A formalization and proof checker for Isabelle's metalogic