Subresultants

Sebastiaan Joosten and René Thiemann and Akihisa Yamada
Archive of Formal Proofs 2017.

AFP entry

Abstract

We formalize the theory of subresultants and the subresultant polynomial remainder sequence as described by Brown and Traub. As a result, we obtain efficient certified algorithms for computing the resultant and the greatest common divisor of polynomials.

BibTex

@inproceedings{JoostenCPP2017,
author = {Jos{\'{e}} Divas{\'{o}}n and Sebastiaan J. C. Joosten and Ren{\'{e}} Thiemann and Akihisa Yamada},
title = {A Formalization of the {B}erlekamp--{Z}assenhaus Factorization Algorithm},
booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
series = {CPP 2017},
year = {2017},
isbn = {978-1-4503-4705-1},
location = {Paris, France},
pages = {17--29},
numpages = {13},
url = {http://doi.acm.org/10.1145/3018610.3018617},
doi = {10.1145/3018610.3018617},
acmid = {3018617},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Isabelle, Polynomial Factorization, Prime Fields}
}