Formally verified arithmetic

Gerard Huet (
Tue, 29 Nov 94 18:27:58 +0100

Hello. I am conducting an informal survey on formally verified arithmetic
in computer proof assistants. I am interested in receiving short
statements about the state of the art in the various implementations.

This may concern several aspects:
* number theory (chinese remainder, fund. th. of arithmetic, etc)
* rational arithmetic
* axiomatisations of reals (Landau, etc)
* implementations of decision procedures (Tarski, Presburger, inf-sup, ...)
* constructive analysis
* arbitrary precision packages for reals (Boehm, Vuillemin, ...)
* floating-point algorithms validation

Please send your data (preferably one or 2 pages of ascii or tex source,
no gigabytes of libraries or huge ps documents) to

After all, if we are ever going to share mathematical libraries, we might
as well start with arithmetic, which everyone needs, for math or programming.

Thank you for your help.
I shall summarize your sendings on this list.
Gerard Huet