Email Gateway (Feb 20 2024 at 15:07): Email Gateway (Feb 20 2024 at 15:07):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new and substantial contribution, by Jakob Schulz and Emin Karayel:
Karatsuba Multiplication on Integers
We give a verified implementation of the Karatsuba Multiplication on Integers as well as verified runtime bounds. Integers are represented as LSBF (least significant bit first) boolean lists, on which the algorithm by Karatsuba is implemented. The running time of O(n^{\log_2 3}) is verified using the Time Monad defined in Root-Balanced Trees by Nipkow.
It is now online at https://www.isa-afp.org/entries/Karatsuba.html
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC