The Isabelle Framework (Q3543647): Difference between revisions

@@ 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 @@
+Tame Graphs
@@ Property / describes a project that uses: Tame Graphs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Metis_
@@ Property / describes a project that uses: Metis_ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Proof General
@@ Property / describes a project that uses: Proof General / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Locales
@@ Property / describes a project that uses: Locales / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/ZF
@@ Property / describes a project that uses: Isabelle/ZF / 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/978-3-540-71067-7_7
+Normal rank
@@ Property / OpenAlex ID @@
+W1571434026
@@ Property / OpenAlex ID: W1571434026 / rank @@
+Normal rank
@@ Property / cites work @@
+A Compiled Implementation of Normalization by Evaluation
+Normal rank
@@ Property / cites work @@
+Formal Pervasive Verification of a Paging Mechanism
+Normal rank
@@ Property / cites work @@
+Q2729065
@@ Property / cites work: Q2729065 / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+Q4790652
@@ Property / cites work: Q4790652 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754030
@@ Property / cites work: Q2754030 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736387
@@ Property / cites work: Q4736387 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945200
@@ Property / cites work: Q4945200 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic-Free Reasoning in Isabelle/Isar
@@ Property / cites work: Logic-Free Reasoning in Isabelle/Isar / rank @@
+Normal rank
@@ Property / cites work @@
+Q3431400
@@ Property / cites work: Q3431400 / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Context Aware Calculation and Deduction
@@ Property / cites work: Context Aware Calculation and Deduction / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / 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 @@
+Local Theory Specifications in Isabelle/Isar
@@ Property / cites work: Local Theory Specifications in Isabelle/Isar / rank @@
+Normal rank
@@ Property / cites work @@
+Partial Recursive Functions in Higher-Order Logic
@@ Property / cites work: Partial Recursive Functions in Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+HOLCF = HOL + LCF
@@ Property / cites work: HOLCF = HOL + LCF / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435474
@@ Property / cites work: Q4435474 / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck I: Tame Graphs
@@ Property / cites work: Flyspeck I: Tame Graphs / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck II: The basic linear programs
@@ Property / cites work: Flyspeck II: The basic linear programs / rank @@
+Normal rank
@@ Property / cites work @@
+Natural deduction as higher-order resolution
@@ Property / cites work: Natural deduction as higher-order resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory for verification. I: From foundations to functions
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory for verification. II: Induction and recursion
+Normal rank
@@ Property / cites work @@
+Q4520767
@@ Property / cites work: Q4520767 / rank @@
+Normal rank
@@ Property / cites work @@
+The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
+Normal rank
@@ Property / cites work @@
+Organizing numerical theories using axiomatic type classes
+Normal rank
@@ Property / cites work @@
+Source-Level Proof Reconstruction for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Types, bytes, and separation logic
@@ Property / cites work: Types, bytes, and separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank
@@ Property / cites work @@
+Structured Induction Proofs in Isabelle/Isar
@@ Property / cites work: Structured Induction Proofs in Isabelle/Isar / rank @@
+Normal rank
@@ Property / cites work @@
+Building Formal Method Tools in the Isabelle/Isar Framework
+Normal rank
@@ Property / cites work @@
+A comparison of Mizar and Isar
@@ Property / cites work: A comparison of Mizar and Isar / rank @@
+Normal rank