A verified efficient implementation of the LLL basis reduction algorithm

DOI10.29007/XWWHMaRDI QIDQ5222951zbMATH OpenOpenAlexFDO

Authors Ralph Bottesch, Max W. Haslbeck, René Thiemann

Publication date 4 July 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/xwwh

zbMATH Keywords

complexityIsabelle/HOLlattice basis reduction

Mathematics Subject Classification ID

Recommendations

• A formalization of the LLL basis reduction algorithm
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• An LLL algorithm with quadratic complexity
• Lattice basis reduction. An introduction to the LLL algorithm and its applications
• Faster LLL-type Reduction of Lattice Bases

Cited in

(9)

• A formalization of the LLL basis reduction algorithm
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• A formalization of the Smith normal form in higher-order logic
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
• LLL reducing with the most significant bits
• scientific article; zbMATH DE number 1852138 (Why is no real title available?)
• Formalizing Coppersmith's method in Isabelle/HOL
• Formalizing the hidden number problem in Isabelle/HOL
• The Hidden Number Problem

Describes a project that uses

Uses Software

• Jordan Normal Forms
• Isabelle
• Isabelle/HOL
• fpLLL
• Verified LLL
• HOL

This page was built for publication: A verified efficient implementation 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 Q5222951)