| 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 Connect in order to contact the contributor
Submitted on : Friday, April 28, 2006 - 7:12:19 PM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Saturday, April 3, 2010 - 9:46:38 PM
Contributor : Assia Mahboubi Connect in order to contact the contributor
Submitted on : Friday, April 28, 2006 - 7:12:19 PM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Saturday, April 3, 2010 - 9:46:38 PM