The following pages link to Isabelle/HOL (Q14275):
Displaying 50 items.
- A formalization of Dedekind domains and class groups of global fields (Q2102929) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Binary codes that do not preserve primitivity (Q2104527) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Synchronization modulo \(P\) in dynamic networks (Q2110375) (← links)
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy (Q2117791) (← links)
- A mechanically verified theory of contracts (Q2119969) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- Sound reasoning in \textit{tock}-CSP (Q2120813) (← links)
- Strong eventual consistency of the collaborative editing framework WOOT (Q2121065) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- Automated verification of the parallel Bellman-Ford algorithm (Q2145339) (← links)
- A formal semantics of the GraalVM intermediate representation (Q2147184) (← links)
- A verified decision procedure for orders in Isabelle/HOL (Q2147186) (← links)
- Information-flow control on ARM and POWER multicore processors (Q2147697) (← links)
- Formalized soundness and completeness of epistemic logic (Q2148773) (← links)
- Voting theory in the Lean theorem prover (Q2148823) (← links)
- Loop verification with invariants and contracts (Q2152642) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- Stateful protocol composition (Q2167741) (← links)
- CryptHOL: game-based proofs in higher-order logic (Q2175214) (← links)
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (Q2180230) (← links)
- Verifying randomised social choice (Q2180231) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Formal reasoning under cached address translation (Q2209539) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- Relational characterisations of paths (Q2210868) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- Unique solutions of contractions, CCS, and their HOL formalisation (Q2216120) (← links)
- Metamath Zero: designing a theorem prover prover (Q2219381) (← links)
- A framework for formal dynamic dependability analysis using HOL theorem proving (Q2219384) (← links)
- Induction with generalization in superposition reasoning (Q2219385) (← links)
- Maintaining a library of formal mathematics (Q2219408) (← links)
- Simple dataset for proof method recommendation in Isabelle/HOL (Q2219413) (← links)
- Deductive stability proofs for ordinary differential equations (Q2233505) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- A Perron-Frobenius theorem for deciding matrix growth (Q2239274) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- Modal Kleene algebra applied to program correctness (Q2281640) (← links)
