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.
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⟩
