A formalization and proof checker for Isabelle's metalogic (Q2108191): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-022-09648-w
@@ Property / DOI: 10.1007/s10817-022-09648-w / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+OpenTheory
@@ Property / describes a project that uses: OpenTheory / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Milawa
@@ Property / describes a project that uses: Milawa / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Metamath Zero
@@ Property / describes a project that uses: Metamath Zero / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nominal Isabelle
@@ Property / describes a project that uses: Nominal Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jitawa
@@ Property / describes a project that uses: Jitawa / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-022-09648-w
+Normal rank
@@ Property / OpenAlex ID @@
+W4312126060
@@ Property / OpenAlex ID: W4312126060 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Self-verification of HOL Light
@@ Property / cites work: Towards Self-verification of HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Concrete Semantics
@@ Property / cites work: Concrete Semantics / rank @@
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754030
@@ Property / cites work: Q2754030 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle's metalogic: formalization and proof checker
+Normal rank
@@ Property / cites work @@
+Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
+Normal rank
@@ Property / cites work @@
+A verified proof checker for higher-order logic
@@ Property / cites work: A verified proof checker for higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+A Consistent Foundation for Isabelle/HOL
@@ Property / cites work: A Consistent Foundation for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Comprehending Isabelle/HOL’s Consistency
@@ Property / cites work: Comprehending Isabelle/HOL’s Consistency / rank @@
+Normal rank
@@ Property / cites work @@
+A consistent foundation for Isabelle/HOL
@@ Property / cites work: A consistent foundation for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Zero’s Solutions for Pollack-Inconsistency
@@ Property / cites work: HOL Zero’s Solutions for Pollack-Inconsistency / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075242
@@ Property / cites work: Q3075242 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4246942
@@ Property / cites work: Q4246942 / rank @@
+Normal rank
@@ Property / cites work @@
+Metamath Zero: designing a theorem prover prover
@@ Property / cites work: Metamath Zero: designing a theorem prover prover / rank @@
+Normal rank
@@ Property / cites work @@
+The reflective Milawa theorem prover is sound (down to the machine code that runs it)
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+A formalized general theory of syntax with bindings: extended version
+Normal rank
@@ Property / cites work @@
+Q3204068
@@ Property / cites work: Q3204068 / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+More Church-Rosser proofs (in Isabelle/HOL)
@@ Property / cites work: More Church-Rosser proofs (in Isabelle/HOL) / rank @@
+Normal rank
@@ Property / cites work @@
+Q4274997
@@ Property / cites work: Q4274997 / rank @@
+Normal rank
@@ Property / cites work @@
+Type Reconstruction for Type Classes
@@ Property / cites work: Type Reconstruction for Type Classes / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736387
@@ Property / cites work: Q4736387 / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Seventy-five problems for testing automatic theorem provers
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+The Isabelle Collections Framework
@@ Property / cites work: The Isabelle Collections Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
+Normal rank
@@ Property / DOI @@
+.1007/S10817-022-09648-W
@@ Property / DOI: 10.1007/S10817-022-09648-W / rank @@
+Normal rank