A formalization of the LLL basis reduction algorithm

DOI10.1007/978-3-319-94821-8_10MaRDI QIDQ1791154zbMATH OpenOpenAlexFDO

Authors Jose Divasón, René Thiemann, Akihisa Yamada, Sebastiaan J. C. Joosten

Publication date 4 October 2018

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_10

Mathematics Subject Classification ID

Lattices and convex bodies (number-theoretic aspects) (11H06) Number-theoretic algorithms; complexity (11Y16) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A verified efficient implementation of the LLL basis reduction algorithm
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• Lattice basis reduction. An introduction to the LLL algorithm and its applications
• Matrices and the LLL algorithm
• An LLL algorithm with quadratic complexity

Cited in

(7)

• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• A verified efficient implementation of the LLL basis reduction algorithm
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• scientific article; zbMATH DE number 1852138 (Why is no real title available?)
• Optimal systems of fundamental \(S\)-units for LLL-reduction
• LLL reducing with the most significant bits
• Formalizing Coppersmith's method in Isabelle/HOL

Describes a project that uses

Uses Software

• Vector Spaces
• Verified LLL
• LLL Factorization
• Berlekamp Zassenhaus
• fpLLL
• HOL Light
• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: A formalization of the LLL basis reduction algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791154)