A formalization and proof checker for Isabelle's metalogic
type: Item
instance of: scholarly article
title: A formalization and proof checker for Isabelle's metalogic
zbMATH Open document ID: 1502.68353
author: Simon Roßkopf
author: Tobias Nipkow
published in: Journal of Automated Reasoning
publication date: 2022-12-19T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7634129
zbMATH Keywords: theorem proving
zbMATH Keywords: higher-order logic
zbMATH Keywords: Isabelle
zbMATH Keywords: proof checker
zbMATH Keywords: metalogic
describes a project that uses: Isabelle
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL Zero
describes a project that uses: Lifting
describes a project that uses: CakeML
describes a project that uses: Twelf
describes a project that uses: Elf
describes a project that uses: OpenTheory
describes a project that uses: Coq
describes a project that uses: Milawa
describes a project that uses: Metamath Zero
describes a project that uses: Transfer
describes a project that uses: Nominal Isabelle
describes a project that uses: Jitawa
MaRDI profile type: Publication
full work available at URL: s10817-022-09648-w
OpenAlex ID: W4312126060
cites work: Towards Self-verification of HOL Light
cites work: Isabelle. A generic theorem prover
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Concrete Semantics
cites work: The foundation of a generic theorem prover
cites work: Q2754030
cites work: Isabelle's metalogic: formalization and proof checker
cites work: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
cites work: A verified proof checker for higher-order logic
cites work: A Consistent Foundation for Isabelle/HOL
cites work: Comprehending Isabelle/HOL’s Consistency
cites work: A consistent foundation for Isabelle/HOL
cites work: HOL Zero’s Solutions for Pollack-Inconsistency
cites work: Q3075242
cites work: Q4246942
cites work: Metamath Zero: designing a theorem prover prover
cites work: The reflective Milawa theorem prover is sound (down to the machine code that runs it)
cites work: Nominal techniques in Isabelle/HOL
cites work: A formalized general theory of syntax with bindings: extended version
cites work: Q3204068
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: More Church-Rosser proofs (in Isabelle/HOL)
cites work: Q4274997
cites work: Type Reconstruction for Type Classes
cites work: Constructive Type Classes in Isabelle
cites work: Q4736387
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: Data Refinement in Isabelle/HOL
cites work: Seventy-five problems for testing automatic theorem provers
cites work: CakeML
cites work: The Isabelle Collections Framework
cites work: Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
DOI: 10.1007/S10817-022-09648-W
description: scientific article; zbMATH DE number 7634129