Formally verified certificate checkers for hardest-to-round computation
From MaRDI portal
Publication:2352500
DOI10.1007/S10817-014-9312-2zbMath1315.68222OpenAlexW2043168300MaRDI QIDQ2352500
Laurent Théry, Micaela Mayero, Érik Martin-Dorel, Guillaume Hanrot
Publication date: 2 July 2015
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00919498/file/Hensel-JAR.pdf
Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Error analysis and interval analysis (65G99)
Related Items (2)
A verified implementation of the Berlekamp-Zassenhaus factorization algorithm ⋮ Formally Verified Approximations of Definite Integrals
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- On the adjugate matrix
- Factoring polynomials with rational coefficients
- Small solutions to polynomial equations, and low exponent RSA vulnerabilities
- A Hensel lifting to replace factorization in list-decoding of algebraic-geometric and Reed-Solomon codes
- Finding a Small Root of a Univariate Modular Equation
- Finding a Small Root of a Bivariate Integer Equation; Factoring with High Bits Known
- A Refinement-Based Approach to Computational Algebra in Coq
- Refinements for Free!
- Simplified High-Speed High-Distance List Decoding for Alternant Codes
- Searching worst cases of a one-variable function using lattice reduction
- Canonical Big Operators
- First-Class Type Classes
- Handbook of Floating-Point Arithmetic
- Improved decoding of Reed-Solomon and algebraic-geometry codes
- Automatic Data Refinement
- Data Refinement in Isabelle/HOL
- Types for Proofs and Programs
- Finding smooth integers in short intervals using CRT decoding
- Algorithmic Number Theory
This page was built for publication: Formally verified certificate checkers for hardest-to-round computation
