The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS (Q2940885) (← links)
- On Rely-Guarantee Reasoning (Q2941165) (← links)
- A Program Construction and Verification Tool for Separation Logic (Q2941173) (← links)
- Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface (Q2945623) (← links)
- A Formalized Hierarchy of Probabilistic System Types (Q2945633) (← links)
- A Verified Enclosure for the Lorenz Attractor (Rough Diamond) (Q2945634) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Stream Fusion for Isabelle’s Code Generator (Q2945639) (← links)
- Amortized Complexity Verified (Q2945642) (← links)
- Deriving Comparators and Show Functions in Isabelle/HOL (Q2945654) (← links)
- Formalising Knot Theory in Isabelle/HOL (Q2945656) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Mechanizing the metatheory of LF (Q2946633) (← links)
- Taming Paraconsistent (and Other) Logics (Q2946751) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion (Q2958390) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
- A Discrete Geometric Model of Concurrent Program Execution (Q2971172) (← links)
- Towards a UTP Semantics for Modelica (Q2971175) (← links)
- An Axiomatic Value Model for Isabelle/UTP (Q2971180) (← links)
- UTPCalc — A Calculator for UTP Predicates (Q2971182) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Foundational extensible corecursion: a proof assistant perspective (Q2981955) (← links)
- Refinement through restraint: bringing down the cost of verification (Q2982005) (← links)
- (Q2985126) (← links)
- Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (Q2986838) (← links)
- A Lambda-Free Higher-Order Recursive Path Order (Q2988386) (← links)
- Friends with Benefits (Q2988636) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- (Q2989002) (← links)
- Data Refinement of Invariant Based Programs (Q2994494) (← links)
- Guarded Operations, Refinement and Simulation (Q2994496) (← links)
- Psi-calculi: a framework for mobile processes with nominal data and logic (Q3003314) (← links)
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs (Q3003486) (← links)
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL (Q3007567) (← links)
- The representational adequacy of <scp>Hybrid</scp> (Q3008233) (← links)
- Saoithín: A Theorem Prover for UTP (Q3055742) (← links)
- Unifying Theories in Isabelle/HOL (Q3055747) (← links)
- Termination Graphs for Java Bytecode (Q3058449) (← links)
- Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) (Q3058454) (← links)
- Second-Order Programs with Preconditions (Q3058455) (← links)
- (Q3062059) (← links)
- The TPTP World – Infrastructure for Automated Reasoning (Q3066085) (← links)
- From a Proven Correct Microkernel to Trustworthy Large Systems (Q3067529) (← links)
- Logical Formalisation and Analysis of the Mifare Classic Card in PVS (Q3087992) (← links)
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments (Q3087999) (← links)
