Karatsuba Multiplication on Integers

Jakob Schulz 📧 and Emin Karayel 📧

February 19, 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.

Abstract

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.

License

BSD License

Topics

Related publications

  • https://mediatum.ub.tum.de/doc/1717658/1717658.pdf

Session Karatsuba

Depends on

Used by

Cite

× 
@article{Karatsuba-AFP,
  author  = {Jakob Schulz and Emin Karayel},
  title   = {Karatsuba Multiplication on Integers},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Karatsuba.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: