The following pages link to Isabelle (Q13212):
Displaying 50 items.
- A simple formalization and proof for the multilated chess board (Q2720299) (← links)
- (Q2722012) (← links)
- (Q2722041) (← links)
- (Q2723408) (← links)
- (Q2723411) (← links)
- (Q2723417) (← links)
- (Q2723890) (← links)
- (Q2729065) (← links)
- (Q2729071) (← links)
- (Q2739733) (← links)
- Logical frameworks (Q2751369) (← links)
- Encoding two-valued nonclassical logics in classical logic (Q2751373) (← links)
- \(\mu\)Java: Embedding a programming language in a theorem prover (Q2752051) (← links)
- (Q2754030) (← links)
- (Q2754041) (← links)
- (Q2754051) (← links)
- (Q2754058) (← links)
- (Q2754063) (← links)
- (Q2754065) (← links)
- (Q2763959) (← links)
- (Q2764132) (← links)
- (Q2766799) (← links)
- (Q2767085) (← links)
- A formal framework for managing mathematics (Q2767940) (← links)
- (Q2769440) (← links)
- (Q2769442) (← links)
- (Q2778886) (← links)
- Dynamic asset allocation in a mean-variance framework (Q2784078) (← links)
- Adding metatheoretic facilities to first-order theories (Q2785674) (← links)
- A Verified Compiler for Probability Density Functions (Q2802431) (← links)
- Automating soundness proofs (Q2810691) (← links)
- Isabelle/UTP: A Mechanised Theory Engineering Framework (Q2814613) (← links)
- Formalization of Normal Random Variables in HOL (Q2817293) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Translating Scala Programs to Isabelle/HOL (Q2817953) (← links)
- Automating Free Logic in Isabelle/HOL (Q2819197) (← links)
- Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0 (Q2819200) (← links)
- Automated theorem proving for special functions: the next phase (Q2819703) (← links)
- A scalable, correct time-stamped stack (Q2819810) (← links)
- Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification (Q2827442) (← links)
- An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
- Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency (Q2829245) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← 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)
