Karatsuba Multiplication on Integers (Q7361095)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Karatsuba
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Karatsuba Multiplication on Integers |
AFP entry Karatsuba |
Statements
19 February 2024
0 references
Jakob Schulz
0 references
Emin Karayel
0 references
Karatsuba Multiplication on Integers (English)
0 references
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\left(n^{\log_2 3}\right)$ is verified using the Time Monad defined in Root-Balanced Trees by Nipkow.
0 references
