coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Micaela Mayero <Micaela.Mayero AT inria.fr>
- To: aaa AT dcs.st-and.ac.uk (Andrew Adams)
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: Real Numbers in Coq
- Date: Thu, 28 Sep 2000 22:09:13 +0200 (MET DST)
> Dear All,
>
> I've been hearing word of a development of the real numbers and real
> analysis in Coq for the last few months, but I can't find any concrete
> references to the work. Can someone provide a pointer to any published or
> unpublished research papers on this, or even just the contact name of the
> developer? We've been developing real analysis in PVS and there've been a
> number of other provers with real number/analysis developments recently
> and I'm trying to keep up with them.
Hello,
Currently, there are, at least, two publications about the real numbers
in Coq: it is an example of use of this developpement to prove the three
gap theorem (Steinhauss conjecture). The research report deals more with Coq
and the real numbers. The paper is about the theorem itself.
ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-3848.ps.gz
ftp://ftp.inria.fr/INRIA/Projects/coq/Micaela.Mayero/PS/three-gap.ps.tar.gz
There is also some people at INRIA Sophia-Antipolis who work with real
numbers in Coq (you can contact Loic Pottier:
http://www-sop.inria.fr/lemme/Loic.Pottier/home.html).
A first version of this developpement, with basic lemmas, lemmas about the
integer and fractional parts, developpements about limits and derivative is
available with the Coq V6.3.1 distribution:
http://coq.inria.fr/
We can also see the real numbers theory specification on line at:
http://coq.inria.fr/library/REALS/
This work is in progress, and a new corrected version, more concise and
extended will be provided in the next version of Coq (V7).
If you have questions (or remarks), I'll be happy to answer.
Best Regards,
Micaela.
=============================================================================
Micaela Mayero <Email>:
Micaela.Mayero AT inria.fr
<Laboratory>: The Coq Project <Domain>: Formal Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
FRANCE
<Tel>: (33)-(0)1 39 63 57 51
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~mayero
=============================================================================
- Real Numbers in Coq, Andrew Adams
- Re: Real Numbers in Coq, Micaela Mayero
Archive powered by MhonArc 2.6.16.