The following pages link to Isabelle/HOL (Q14275):
Displaying 18 items.
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- Organizing numerical theories using axiomatic type classes (Q1774558) (← links)
- Relation algebra as programming language using the Ampersand compiler (Q1785856) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite (Q2655324) (← links)
- Automated theorem proving for special functions (Q2819703) (← links)
- An Isabelle/HOL Formalisation of Green’s Theorem (Q2829238) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets (Q2890328) (← links)
- Guarded Operations, Refinement and Simulation (Q2994496) (← links)
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms (Q3453644) (← links)
- A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi (Q5179010) (← links)
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (Q5371950) (← links)
- A trusted mechanised JavaScript specification (Q5408408) (← links)
- A Formal Language for Cryptographic Pseudocode (Q5505567) (← links)
- A formal proof of the expressiveness of deep learning (Q5919583) (← links)
