The following pages link to HOL (Q17631):
Displaying 50 items.
- Formal verification of a partial-order reduction technique for model checking (Q1961915) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- A graph library for Isabelle (Q2018659) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (Q2031406) (← links)
- Mechanisation of the AKS algorithm (Q2031415) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification (Q2038037) (← links)
- Hoare-style logic for unstructured programs (Q2038040) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- Guiding an automated theorem prover with neural rewriting (Q2104548) (← links)
- Strong eventual consistency of the collaborative editing framework WOOT (Q2121065) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- Formalization of RBD-based cause consequence analysis in HOL (Q2128793) (← links)
- A language with type-dependent equality (Q2128827) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← 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)
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} (Q2198134) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← 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)
- Relational characterisations of paths (Q2210868) (← links)
- Unique solutions of contractions, CCS, and their HOL formalisation (Q2216120) (← links)
- A framework for formal dynamic dependability analysis using HOL theorem proving (Q2219384) (← links)
- Induction with generalization in superposition reasoning (Q2219385) (← links)
- Tree neural networks in HOL4 (Q2219410) (← links)
- Simple dataset for proof method recommendation in Isabelle/HOL (Q2219413) (← links)
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM (Q2233462) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings (Q2250560) (← 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)
- An algebra of synchronous atomic steps (Q2281642) (← links)
- Formalization of function matrix theory in HOL (Q2294128) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Priority inheritance protocol proved correct (Q2303234) (← links)
- Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (Q2303242) (← links)
