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

Érik Martin-Dorel 1, 2, *
* Corresponding author
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
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 : Thursday, February 7, 2019 - 3:43:24 PM
Long-term archiving on : 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

336

Files downloads

157