HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 : Friday, February 4, 2022 - 3:23:38 AM
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