Schönhage-Strassen Multiplication

Jakob Schulz 📧

May 10, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We give a verified implementation of the Schönhage-Strassen Multiplication on Integers based on the original paper by Schönhage and Strassen and verify its asymptotic complexity of $\mathcal{O}\left(n \log n \log \log n\right)$ bit operations. Integers are represented as LSBF (least significant bit first) boolean lists. The running time is verified using the Time Monad defined in Root-Balanced Trees by Nipkow. For verifying correctness, we adapt the formalization of Number Theoretic Transforms (NTTs) by Ammer and Kreuzer to the context of rings that need not be fields.


BSD License


Related publications


Session Schoenhage_Strassen