Proving formally the implementation of an efficient gcd algorithm for polynomials - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2006

Proving formally the implementation of an efficient gcd algorithm for polynomials

Assia Mahboubi
Mathematical, Reasoning and Software

Résumé

We describe here a formal proof in the Coq system of the structure theorem for subresultants, which allows to prove formally the correction of our implementation of the subresultant algorithm. Up to our knowledge, it is the first mechanized proof of this result.

Domaines

Logique en informatique [cs.LO]
Fichier principal
Vignette du fichier
SousRes.pdf (159.24 Ko) Télécharger le fichier

Assia Mahboubi  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00001270

Soumis le : vendredi 28 avril 2006-19:12:19

Dernière modification le : mercredi 15 mars 2023-08:58:09

Archivage à long terme le : samedi 3 avril 2010-21:46:38

Télécharger pour visualiser

Dates et versions

inria-00001270 , version 1 (28-04-2006)

Identifiants

  • HAL Id : inria-00001270 , version 1

Citer

Assia Mahboubi. Proving formally the implementation of an efficient gcd algorithm for polynomials. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Aug 2006, Seattle, WA, United States. pp.438-452. ⟨inria-00001270⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

INRIA INRIA2
111 Consultations
446 Téléchargements

Partager

Gmail Facebook X LinkedIn More