Cited in
(29)- Comprehending Isabelle/HOL’s Consistency
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
- From types to sets by local type definition in higher-order logic
- A formalization of the Smith normal form in higher-order logic
- A verified implementation of algebraic numbers in Isabelle/HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- A formalization of the LLL basis reduction algorithm
- Classification of finite fields with applications
- HOL-Omega
- Cayley-Hamilton
- TiML
- LLL Factorization
- Perron Frobenius
- Root Balanced Tree
- Verified LLL
- Vector Spaces
- Landau Symbols
- Median-of-Medians
- Auto2_Imperative_HOL
- Count Complex Roots
- Linear Recurrences
- Sqrt_Babylonian
- finfield.v
- Probabilistic_While
- Verifying asymptotic time complexity of imperative programs in Isabelle
- From LCF to Isabelle/HOL
- Hermite
- Modular_arithmetic_LLL_and_HNF_algorithms
- Smith_Normal_Form
This page was built for software: Berlekamp Zassenhaus
