From owner-qed Tue Nov 29 11:28:34 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA15756 for qed-out; Tue, 29 Nov 1994 11:28:07 -0600
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id LAA15748 for <qed@mcs.anl.gov>; Tue, 29 Nov 1994 11:28:00 -0600
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.6.9/8.6.9) with SMTP id SAA20718 for <qed@mcs.anl.gov>; Tue, 29 Nov 1994 18:27:58 +0100
Received: by pauillac.inria.fr; Tue, 29 Nov 94 18:27:58 +0100
Date: Tue, 29 Nov 94 18:27:58 +0100
From: Gerard Huet <Gerard.Huet@inria.fr>
Message-Id: <9411291727.AA04859@pauillac.inria.fr>
To: qed@mcs.anl.gov
Subject: Formally verified arithmetic
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

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 Gerard.Huet@inria.fr

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