Read about our upcoming Code of Conduct on this issue

Commit cc0a4216 authored by Andreas Lochbihler's avatar Andreas Lochbihler
Browse files

metadata for Modular_arithmetic_LLL_and_HNF_algorithms

parent 05123cb597d8
......@@ -10379,3 +10379,23 @@ abstract =
We use Isabelle/HOL to verify elementary theorems and alternative
axiomatizations of classical extensional mereology.
title = Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
author = Ralph Bottesch, Jose Divason, Rene Thiemann <>
topic = Computer science/Algorithms/Mathematical
date = 2021-03-12
notify =
abstract =
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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment