| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Proving formally the implementation of an efficient gcd algorithm for polynomials
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.
Cited literature [18 references]
https://hal.inria.fr/inria-00001270
Contributor : Assia Mahboubi <>
Submitted on : Friday, April 28, 2006 - 7:12:19 PM
Last modification on : Thursday, March 5, 2020 - 5:34:25 PM
Document(s) archivé(s) le : Saturday, April 3, 2010 - 9:46:38 PM
Contributor : Assia Mahboubi <>
Submitted on : Friday, April 28, 2006 - 7:12:19 PM
Last modification on : Thursday, March 5, 2020 - 5:34:25 PM
Document(s) archivé(s) le : Saturday, April 3, 2010 - 9:46:38 PM