The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started (Q2657827) (← links)
- Klein-Beltrami model. III (Q2658806) (← links)
- Klein-Beltrami model. IV (Q2658807) (← links)
- Binary intersection formalized (Q2662679) (← links)
- Certified quantum computation in Isabelle/HOL (Q2666954) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- EthVer: formal verification of randomized Ethereum smart contracts (Q2670859) (← links)
- The refinement calculus of reactive systems (Q2672236) (← links)
- Strategyproof social choice when preferences and outcomes may contain ties (Q2673159) (← links)
- A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
- WhyMP, a formally verified arbitrary-precision integer library (Q2673999) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- Second-order properties of undirected graphs (Q2695354) (← links)
- Relation-algebraic verification of Borůvka's minimum spanning tree algorithm (Q2695356) (← links)
- Automated reasoning for probabilistic sequential programs with theorem proving (Q2695373) (← links)
- Type-theoretic approaches to ordinals (Q2700785) (← links)
- (Q2722012) (← links)
- (Q2723408) (← links)
- (Q2723411) (← links)
- \(\mu\)Java: Embedding a programming language in a theorem prover (Q2752051) (← links)
- (Q2754040) (← links)
- (Q2754041) (← links)
- (Q2754058) (← links)
- (Q2754065) (← links)
- (Q2763959) (← links)
- (Q2766799) (← links)
- (Q2769440) (← links)
- (Q2769442) (← links)
- (Q2778886) (← links)
- On Logic Embeddings and Gödel’s God (Q2787333) (← links)
- From Sets to Bits in Coq (Q2798253) (← links)
- Proof–Based Synthesis of Sorting Algorithms for Trees (Q2798749) (← links)
- Overview of the Mathemagix Type System (Q2799572) (← links)
- A Verified Compiler for Probability Density Functions (Q2802431) (← links)
- Witnessing (Co)datatypes (Q2802441) (← links)
- Binding Structures as an Abstract Data Type (Q2802464) (← links)
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic (Q2802495) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- The Expressive Power of Monotonic Parallel Composition (Q2802500) (← links)
- Reasoning in Abella about structural operational semantics specifications (Q2804943) (← links)
- Automating soundness proofs (Q2810691) (← links)
- Termination Proofs for Recursive Functions in FoCaLiZe (Q2814388) (← links)
- Isabelle/UTP: A Mechanised Theory Engineering Framework (Q2814613) (← links)
- Constructing the Views Framework (Q2814615) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi (Q2817943) (← links)
- Automating Free Logic in Isabelle/HOL (Q2819197) (← links)
