Skip to Main content Skip to Navigation

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 metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Érik Martin-Dorel Connect in order to contact the contributor
Submitted on : Friday, March 11, 2011 - 12:10:51 AM
Last modification on : Thursday, September 29, 2022 - 2:58:07 PM
Long-term archiving on: : Thursday, November 8, 2012 - 11:31:11 AM


Files produced by the author(s)


  • HAL Id : ensl-00575673, version 1



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



Record views


Files downloads