Wiki Agenda Contact Version française

An Efficient Arbitrary-Precision Integer Library

An arbitrary-precision integer library in the style of GMP, designed to be both efficient and formally proved correct.

Authors: Raphaël Rieu-Helft

Topics: Arithmetic / Pointer Programs / Proofs by reflection / Non-linear Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

This library implements arbitrary-precision integers in the style of GMP. Supported operations are addition, multiplication, division, comparisons, shifts square root and modular exponentiation on non-negative integers, as well as some basic operations on relative integers.

More detailed information on the C library is available in the WhyMP repository, as well as in the papers: