Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Two algorithms based on modula...

view this post on Zulip Email Gateway (Mar 14 2021 at 11:13):

From: Andreas Lochbihler <>
I'm happy to announce another AFP entry this week:

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal
form computation

by Ralph Bottesch, Jose Divason and Rene Thiemann

We verify two algorithms for which modular arithmetic plays an essential role:
Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm
for computing the Hermite normal form of a matrix. To do this, we also formalize some
facts about the modulo operation with symmetric range. Our implementations are based on
the original papers, but are otherwise efficient. For basis reduction we formalize two
versions: one that includes all of the optimizations/heuristics from Storjohann's paper,
and one excluding a heuristic that we observed to often decrease efficiency. We also
provide a fast, self-contained certifier for basis reduction, based on the efficient
Hermite normal form algorithm.


Last updated: Dec 08 2021 at 09:20 UTC