Wiki Agenda Contact English version

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.


Auteurs: Raphaël Rieu-Helft

Catégories: Arithmetic / Pointer Programs / Proofs by reflection / Non-linear Arithmetic

Outils: 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: