A Verified Efficient Implementation of the LLL Basis Reduction Algorithm

DOI10.29007/xwwhzbMath1409.68252OpenAlexW2907172504MaRDI QIDQ5222951

Max W. Haslbeck, Ralph Bottesch, 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

Related Items (3)

Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

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

This page was built for publication: A Verified Efficient Implementation of the LLL Basis Reduction Algorithm