Skip to Main content Skip to Navigation
Reports

Univariate and bivariate integral roots certificates based on Hensel's lifting

Érik Martin-Dorel 1, 2, *
* Corresponding author
1 ARENAIRE - Computer arithmetic
LIP - Laboratoire de l'Informatique du Parallélisme, Inria Grenoble - Rhône-Alpes
2 ARENAIRE - Arithmétique des ordinateurs
ENS Lyon - École normale supérieure - Lyon
Abstract : If it is quite easy to check a given integer is a root of a given polynomial with integer coefficients, verifying we know all the integral roots of a polynomial requires a different approach. In both univariate and bivariate cases, we introduce a type of integral roots certificates and the corresponding checker specification, based on Hensel's lifting. We provide a formalization of this iterative algorithm from which we deduce a formal proof of the correctness of the checkers, with the help of the COQ proof assistant along with the SSReflect extension. The ultimate goal of this work is to provide a component that will be involved in a complete certification chain for solving the Table Maker's Dilemma in an exact way.
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00575673
Contributor : Érik Martin-Dorel <>
Submitted on : Friday, March 11, 2011 - 12:10:51 AM
Last modification on : Wednesday, November 20, 2019 - 2:45:34 AM
Document(s) archivé(s) le : Thursday, November 8, 2012 - 11:31:11 AM

File

RRLIP2011-1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : ensl-00575673, version 1

Collections

Citation

Érik Martin-Dorel. Univariate and bivariate integral roots certificates based on Hensel's lifting. 2011. ⟨ensl-00575673⟩

Share

Metrics

Record views

350

Files downloads

171