The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Point-Free, Set-Free Concrete Linear Algebra (Q3088000) (← links)
- Termination of Isabelle Functions via Termination of Rewriting (Q3088004) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism (Q3088012) (← links)
- seL4 Enforces Integrity (Q3088017) (← links)
- Lem: A Lightweight Tool for Heavyweight Semantics (Q3088021) (← links)
- Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers (Q3088023) (← links)
- Formalising foundations of mathematics (Q3094180) (← links)
- Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (Q3095242) (← links)
- Algebra of Monotonic Boolean Transformers (Q3098056) (← links)
- Mechanical Analysis of Finite Idempotent Relations (Q3100172) (← links)
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem (Q3100205) (← links)
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- Proof Pearl: The Marriage Theorem (Q3100219) (← links)
- Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL (Q3102733) (← links)
- Expressing Polymorphic Types in a Many-Sorted Language (Q3172884) (← links)
- Generalized and Formalized Uncurrying (Q3172898) (← links)
- Introduction to Model Checking (Q3176359) (← links)
- Combining Model Checking and Deduction (Q3176378) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm (Q3179390) (← links)
- Specifying Properties of Dynamic Architectures Using Configuration Traces (Q3179403) (← links)
- Unifying Heterogeneous State-Spaces with Lenses (Q3179407) (← links)
- Let’s Get Physical: Models and Methods for Real-World Security Protocols (Q3183515) (← links)
- Turning Inductive into Equational Specifications (Q3183524) (← links)
- Formalizing the Logic-Automaton Connection (Q3183526) (← links)
- Formalising Observer Theory for Environment-Sensitive Bisimulation (Q3183528) (← links)
- Formal Certification of a Resource-Aware Language Implementation (Q3183530) (← links)
- Types, Maps and Separation Logic (Q3183535) (← links)
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL (Q3183537) (← links)
- Formal Verification of Exact Computations Using Newton’s Method (Q3183542) (← links)
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL (Q3183543) (← links)
- Certification of Termination Proofs Using CeTA (Q3183545) (← links)
- Liveness Reasoning with Isabelle/HOL (Q3183549) (← links)
- Generalized Theoroidal Institution Comorphisms (Q3184726) (← links)
- Heterogeneous Logical Environments for Distributed Specifications (Q3184737) (← links)
- Types, bytes, and separation logic (Q3189788) (← links)
- Unified Classical Logic Completeness (Q3192180) (← links)
- Proving Termination of Programs Automatically with AProVE (Q3192189) (← links)
- Interacting with Modal Logics in the Coq Proof Assistant (Q3194730) (← links)
- Formalization of Abstract State Transition Systems for SAT (Q3224685) (← links)
- A Mechanized Proof of Higman’s Lemma by Open Induction (Q3295156) (← links)
- Proof Verification Technology and Elementary Physics (Q3296311) (← links)
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs (Q3303910) (← links)
- Banishing Ultrafilters from Our Consciousness (Q3305324) (← links)
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments (Q3305694) (← links)
- Formalising the pi-calculus using nominal logic (Q3395094) (← links)
- (Q3400637) (← links)
- Finding and Certifying Loops (Q3401124) (← links)
