Isabelle's metalogic: formalization and proof checker

DOI10.1007/978-3-030-79876-5_6OpenAlexW3164251555MaRDI QIDQ2055847

Tobias Nipkow, Simon Roßkopf

Publication date: 1 December 2021

Full work available at URL: https://arxiv.org/abs/2104.12224

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

The formal verification of the ctm approach to forcing ⋮ Isabelle's metalogic: formalization and proof checker ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• Twelf
• CakeML
• Elf
• Metamath Zero

Cites Work

• 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
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item

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