Browse thread
[Caml-announce] exact real arithmetic
- Jean-Christophe Filliatre
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | NaN-NaN-NaN (NaN:NaN) |
| From: | Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...> |
| Subject: | [Caml-announce] exact real arithmetic |
This is to announce an exact real arithmetic module for ocaml, called
Creal (for Constructive Reals). It is available from here:
http://www.lri.fr/~filliatr/software.en.html
This module provides an abstract data type of real numbers, on which
all operations are exact, and return immediately. When necessary, one
can ask for an approximation of a real number to a given precision and
this triggers all the actual computations, including approximations of
some operands to higher precisions if necessary.
This implementation is based on Valérie Ménissier-Morain PhD thesis
(http://www-calfor.lip6.fr/~vmm/arith_english.html)
The tarball includes an ocaml interface to GMP (GNU Multi Precision
library), mainly written by David Monniaux.
Comments and suggestions are welcome.
--
Jean-Christophe Filliatre (http://www.lri.fr/~filliatr)