Read about our upcoming Code of Conduct on this issue

Commit 5e9c01bc authored by Andreas Lochbihler's avatar Andreas Lochbihler
Browse files

sitegen for Modular_arithmetic_LLL_and_HNF_algorithms

parent 137c96131780
......@@ -101,7 +101,7 @@ MathJax = {
Authors:
</td>
<td class="data">
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
<a href="http://cl-informatik.uibk.ac.at/users/mhaslbeck/">Max W. Haslbeck</a> and
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
</td>
......
......@@ -137,7 +137,7 @@ MathJax = {
<td class="data"><a href="Echelon_Form.html">Echelon_Form</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Smith_Normal_Form.html">Smith_Normal_Form</a> </td></tr>
<td class="data"><a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a>, <a href="Smith_Normal_Form.html">Smith_Normal_Form</a> </td></tr>
......
......@@ -169,7 +169,7 @@ All the results have been applied to improve CeTA, our certifier to validate ter
<td class="data"><a href="Polynomial_Factorization.html">Polynomial_Factorization</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a>, <a href="Farkas.html">Farkas</a>, <a href="Groebner_Bases.html">Groebner_Bases</a>, <a href="Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a>, <a href="Linear_Programming.html">Linear_Programming</a>, <a href="Perron_Frobenius.html">Perron_Frobenius</a>, <a href="QHLProver.html">QHLProver</a>, <a href="Stochastic_Matrices.html">Stochastic_Matrices</a>, <a href="Subresultants.html">Subresultants</a> </td></tr>
<td class="data"><a href="Deep_Learning.html">Deep_Learning</a>, <a href="Farkas.html">Farkas</a>, <a href="Groebner_Bases.html">Groebner_Bases</a>, <a href="Isabelle_Marries_Dirac.html">Isabelle_Marries_Dirac</a>, <a href="Linear_Programming.html">Linear_Programming</a>, <a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a>, <a href="Perron_Frobenius.html">Perron_Frobenius</a>, <a href="QHLProver.html">QHLProver</a>, <a href="Stochastic_Matrices.html">Stochastic_Matrices</a>, <a href="Subresultants.html">Subresultants</a> </td></tr>
......
......@@ -97,7 +97,7 @@ MathJax = {
Authors:
</td>
<td class="data">
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
<a href="https://www.unirioja.es/cu/jodivaso/">Jose Divasón</a>,
<a href="http://cl-informatik.uibk.ac.at/users/mhaslbeck/">Maximilian Haslbeck</a>,
<a href="http://sjcjoosten.nl/">Sebastiaan Joosten</a>,
......@@ -161,7 +161,7 @@ textbook by von zur Gathen and Gerhard.</td>
<td class="data"><a href="Algebraic_Numbers.html">Algebraic_Numbers</a>, <a href="Berlekamp_Zassenhaus.html">Berlekamp_Zassenhaus</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Linear_Inequalities.html">Linear_Inequalities</a>, <a href="LLL_Factorization.html">LLL_Factorization</a> </td></tr>
<td class="data"><a href="Linear_Inequalities.html">Linear_Inequalities</a>, <a href="LLL_Factorization.html">LLL_Factorization</a>, <a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a> </td></tr>
......
......@@ -93,7 +93,7 @@ MathJax = {
Authors:
</td>
<td class="data">
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
Alban Reynaud and
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
</td>
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">T</font>wo
algorithms
based
on
modular
arithmetic:
lattice
basis
reduction
and
<font class="first">H</font>ermite
normal
form
computation
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
Ralph Bottesch,
Jose Divason and
<a href="http://cl-informatik.uibk.ac.at/users/thiemann/">Rene Thiemann</a>
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2021-03-12</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
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.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP,
author = {Ralph Bottesch and Jose Divason and Rene Thiemann},
title = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation},
journal = {Archive of Formal Proofs},
month = mar,
year = 2021,
note = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Hermite.html">Hermite</a>, <a href="Jordan_Normal_Form.html">Jordan_Normal_Form</a>, <a href="LLL_Basis_Reduction.html">LLL_Basis_Reduction</a>, <a href="Show.html">Show</a>, <a href="Smith_Normal_Form.html">Smith_Normal_Form</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Modular_arithmetic_LLL_and_HNF_algorithms/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Modular_arithmetic_LLL_and_HNF_algorithms/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Modular_arithmetic_LLL_and_HNF_algorithms/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Modular_arithmetic_LLL_and_HNF_algorithms-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -152,7 +152,7 @@ datatypes similar to Haskell's "deriving Show".</td>
<td class="data"><a href="Deriving.html">Deriving</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
......
......@@ -166,7 +166,9 @@ the use of local type definitions.</td>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Berlekamp_Zassenhaus.html">Berlekamp_Zassenhaus</a>, <a href="Hermite.html">Hermite</a>, <a href="List-Index.html">List-Index</a>, <a href="Perron_Frobenius.html">Perron_Frobenius</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a> </td></tr>
</tbody>
......
......@@ -88,6 +88,16 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td class="head">2021</td>
</tr>
<tr>
<td class="entry">
2021-03-12: <a href="entries/Modular_arithmetic_LLL_and_HNF_algorithms.html">Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation</a>
<br>
Authors:
Ralph Bottesch,
Jose Divason
and <a href="http://cl-informatik.uibk.ac.at/users/thiemann/">Rene Thiemann</a>
</td>
</tr>
<tr>
<td class="entry">
2021-03-03: <a href="entries/Projective_Measurements.html">Quantum projective measurements and the CHSH inequality</a>
......@@ -1053,7 +1063,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
2019-06-21: <a href="entries/Linear_Inequalities.html">Linear Inequalities</a>
<br>
Authors:
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
Alban Reynaud
and René Thiemann
</td>
......@@ -1239,7 +1249,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
2019-01-17: <a href="entries/Farkas.html">Farkas' Lemma and Motzkin's Transposition Theorem</a>
<br>
Authors:
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
<a href="http://cl-informatik.uibk.ac.at/users/mhaslbeck/">Max W. Haslbeck</a>
and René Thiemann
</td>
......@@ -1756,7 +1766,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
2018-02-02: <a href="entries/LLL_Basis_Reduction.html">A verified LLL algorithm</a>
<br>
Authors:
<a href="http://cl-informatik.uibk.ac.at/users/bottesch/">Ralph Bottesch</a>,
Ralph Bottesch,
<a href="https://www.unirioja.es/cu/jodivaso/">Jose Divasón</a>,
<a href="http://cl-informatik.uibk.ac.at/users/mhaslbeck/">Maximilian Haslbeck</a>,
<a href="http://sjcjoosten.nl/">Sebastiaan Joosten</a>,
......
......@@ -9,7 +9,27 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>03 Mar 2021 00:00:00 +0000</pubDate>
<pubDate>12 Mar 2021 00:00:00 +0000</pubDate>
<item>
<title>Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation</title>
<link>https://www.isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html</link>
<guid>https://www.isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html</guid>
<dc:creator> Ralph Bottesch, Jose Divason, Rene Thiemann </dc:creator>
<pubDate>12 Mar 2021 00:00:00 +0000</pubDate>
<description>
We verify two algorithms for which modular arithmetic plays an
essential role: Storjohann&#39;s variant of the LLL lattice basis
reduction algorithm and Kopparty&#39;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&#39;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.</description>
</item>
<item>
<title>Quantum projective measurements and the CHSH inequality</title>
<link>https://www.isa-afp.org/entries/Projective_Measurements.html</link>
......@@ -570,30 +590,5 @@ href=&#34;https://www.isa-afp.org/entries/Incompleteness.html&#34;&gt;Larry
Paulson’s formalization of the Hereditarily Finite Set
theory&lt;/a&gt;.</description>
</item>
<item>
<title>An Abstract Formalization of G&ouml;del's Incompleteness Theorems</title>
<link>https://www.isa-afp.org/entries/Goedel_Incompleteness.html</link>
<guid>https://www.isa-afp.org/entries/Goedel_Incompleteness.html</guid>
<dc:creator> Andrei Popescu, Dmitriy Traytel </dc:creator>
<pubDate>16 Sep 2020 00:00:00 +0000</pubDate>
<description>
We present an abstract formalization of G&amp;ouml;del&#39;s
incompleteness theorems. We analyze sufficient conditions for the
theorems&#39; applicability to a partially specified logic. Our
abstract perspective enables a comparison between alternative
approaches from the literature. These include Rosser&#39;s variation
of the first theorem, Jeroslow&#39;s variation of the second theorem,
and the Swierczkowski&amp;ndash;Paulson semantics-based approach. This
AFP entry is the main entry point to the results described in our
CADE-27 paper &lt;a
href=&#34;https://dx.doi.org/10.1007/978-3-030-29436-6_26&#34;&gt;A
Formally Verified Abstract Account of Gödel&#39;s Incompleteness
Theorems&lt;/a&gt;. As part of our abstract formalization&#39;s
validation, we instantiate our locales twice in the separate AFP
entries &lt;a
href=&#34;https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html&#34;&gt;Goedel_HFSet_Semantic&lt;/a&gt;
and &lt;a
href=&#34;https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html&#34;&gt;Goedel_HFSet_Semanticless&lt;/a&gt;.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -209,6 +209,7 @@
<a href="entries/Signature_Groebner.html">Signature_Groebner</a> &nbsp;
<a href="entries/Smith_Normal_Form.html">Smith_Normal_Form</a> &nbsp;
<a href="entries/Safe_Distance.html">Safe_Distance</a> &nbsp;
<a href="entries/Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a> &nbsp;
<strong>Optimization:</strong>
<a href="entries/Simplex.html">Simplex</a> &nbsp;
<strong>Quantum computing:</strong>
......
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