The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Agent-Based HOL Reasoning (Q2819202) (← links)
- The GDML and EuKIM Projects: Short Report on the Initiative (Q2819256) (← links)
- Lem: reusable engineering of real-world semantics (Q2819676) (← links)
- Automated theorem proving for special functions: the next phase (Q2819703) (← links)
- Monadic Sequence Testing and Explicit Test-Refinements (Q2827440) (← links)
- An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
- HOL Zero’s Solutions for Pollack-Inconsistency (Q2829240) (← links)
- Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency (Q2829245) (← links)
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl) (Q2829247) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- Visual Theorem Proving with the Incredible Proof Machine (Q2829254) (← links)
- The Flow of ODEs (Q2829258) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- Equational Reasoning with Applicative Functors (Q2829262) (← links)
- Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems (Q2829264) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- A Framework for the Automatic Formal Verification of Refinement from Cogent to C (Q2829268) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Algebraic Numbers in Isabelle/HOL (Q2829274) (← links)
- Formalized Timed Automata (Q2829277) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Formalising Semantics for Expected Running Time of Probabilistic Programs (Q2829281) (← links)
- A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations (Q2841231) (← links)
- The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
- Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts (Q2841233) (← links)
- Ours Is to Reason Why (Q2842639) (← links)
- A Universal Machine for Biform Theory Graphs (Q2843007) (← links)
- Formal Mathematics on Display: A Wiki for Flyspeck (Q2843012) (← links)
- Capturing Hiproofs in HOL Light (Q2843014) (← links)
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory (Q2843015) (← links)
- A new machine-checked proof of strong normalisation for display logic (Q2843910) (← links)
- Grail: a functional form for imperative mobile code (Q2844038) (← links)
- Towards a readable formalisation of category theory (Q2845528) (← links)
- Bounded model generation for Isabelle/HOL (Q2848061) (← links)
- Integrating a SAT solver with an LCF-style theorem prover (Q2848690) (← links)
- MetiTarski’s Menagerie of Cooperating Systems (Q2849476) (← links)
- Mechanizing the Metatheory of Sledgehammer (Q2849493) (← links)
- On the Formal Analysis of Geometrical Optics in HOL (Q2849513) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2863855) (← links)
- Programmed strategies for program verification (Q2864527) (← links)
- Enhancing theorem prover interfaces with program slice information (Q2867933) (← links)
- Web interfaces for proof assistants (Q2867935) (← links)
- Tool support for proof engineering (Q2867938) (← links)
- HOL Based First-Order Modal Logic Provers (Q2870120) (← links)
- Modeling and verifying graph transformations in proof assistants (Q2870320) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- A completeness proof for bisimulation in the pi-calculus using Isabelle (Q2871830) (← links)
