Schönhage-Strassen Multiplication

Jakob Schulz 📧

May 10, 2024


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