Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL


BibTeX

@inproceedings{RTRBJD-JAR20,
author = "René Thiemann and Ralph Bottesch and Jose Divasón and Max W. Haslbeck and Sebastiaan J.C. Joosten and Akihisa Yamada",
title = "Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL",
series = "J Autom Reasoning",
volume = 64,
pages = "827--856",
year = 2020,
doi = "10.1007/s10817-020-09552-1"
}


Nach oben scrollen