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

Érik Martin-Dorel 1, 2, *
* Auteur correspondant
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.
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00575673
Contributeur : Érik Martin-Dorel <>
Soumis le : vendredi 11 mars 2011 - 00:10:51
Dernière modification le : samedi 21 avril 2018 - 01:27:10
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 11:31:11

Fichier

RRLIP2011-1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

318

Téléchargements de fichiers

149