Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

DOI10.1007/978-3-031-38499-8_21MaRDI QIDQ6492756zbMATH OpenFDO

Authors Tobias Nipkow

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_21

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 5485482 (Why is no real title available?)
• scientific article; zbMATH DE number 1224949 (Why is no real title available?)
• scientific article; zbMATH DE number 1256724 (Why is no real title available?)
• scientific article; zbMATH DE number 1775383 (Why is no real title available?)
• scientific article; zbMATH DE number 2120513 (Why is no real title available?)
• scientific article; zbMATH DE number 7699437 (Why is no real title available?)
• Approximate CVP in time \(2^{0.802 n}\) -- now in any norm!
• Approximating CVP to within almost-polynomial factors is NP-hard
• Concrete semantics. With Isabelle/HOL
• Factoring polynomials with rational coefficients
• Hardness of approximating the shortest vector problem in lattices
• Isabelle/HOL. A proof assistant for higher-order logic
• Lattice-based Cryptography
• On Lovász' lattice reduction and the nearest lattice point problem

Cited in

(1)

• Formalizing Coppersmith's method in Isabelle/HOL

This page was built for publication: Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6492756)