Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials

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

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Assia Mahboubi
• Keywords: Automated Reasoning, CADE 2006, Mechanized Proof