A formalization and proof checker for Isabelle's metalogic

DOI10.1007/S10817-022-09648-WzbMATH Open1502.68353OpenAlexW4312126060MaRDI QIDQ2108191FDOQ2108191

Authors: 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

Recommendations

• The foundation of a generic theorem prover
• The Isabelle Framework
• scientific article; zbMATH DE number 1088221
• A verified proof checker for higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic

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)

Cites Work

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Nominal techniques in Isabelle/HOL
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Title not available (Why is that?)
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Metamath Zero: designing a theorem prover prover
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• More Church-Rosser proofs (in Isabelle/HOL)
• Isabelle's metalogic: formalization and proof checker
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Concrete Semantics
• Sets in Coq, Coq in Sets
• Towards Self-verification of HOL Light
• CakeML
• Title not available (Why is that?)
• Constructive Type Classes in Isabelle
• Code generation via higher-order rewrite systems
• The Isabelle collections framework
• The foundation of a generic theorem prover
• A formalized general theory of syntax with bindings: extended version
• Data refinement in Isabelle/HOL
• Seventy-five problems for testing automatic theorem provers
• Title not available (Why is that?)
• A verified proof checker for higher-order logic
• Type Reconstruction for Type Classes
• A consistent foundation for Isabelle/HOL
• A Consistent Foundation for Isabelle/HOL
• Title not available (Why is that?)
• Comprehending Isabelle/HOL’s Consistency
• Title not available (Why is that?)
• HOL Zero’s Solutions for Pollack-Inconsistency

Cited In (3)

• The foundation of a generic theorem prover
• Eisbach: a proof method language for Isabelle
• αCheck: A mechanized metatheory model checker

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2108191)