Proving formally the implementation of an efficient gcd algorithm for polynomials

Assia Mahboubi 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : 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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/inria-00001270
Contributor : Assia Mahboubi <>
Submitted on : Friday, April 28, 2006 - 7:12:19 PM
Last modification on : Thursday, January 11, 2018 - 4:22:00 PM
Document(s) archivé(s) le : Saturday, April 3, 2010 - 9:46:38 PM

Identifiers

  • HAL Id : inria-00001270, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

207

Files downloads

386