A simple and (hopefully) portable floating-point interval arithmetic library in OCaml.
Original repository: https://github.com/monadius/ocaml_simple_interval
-
S. Rump, P. Zimmermann, S. Boldo, G. Melquiond Computing predecessor and successor in rounding to nearest (link2)
-
S. Rump, T. Ogita, Y. Morikura, S. Oishi Interval arithmetic with fixed rounding mode
-
F. Goualard How do you compute the midpoint of an interval?
-
S. Boldo, Dekker algorithm: error of the multiplication. See also S. Boldo, C. Marché, Formal verification of numerical programs: from C annotated programs to mechanical proofs
Interval1 is a simple OCaml interval arithmetic
library which does not depend on any external files and libraries. It
uses the standard rounding to nearest floating-point operations to
compute rigorous interval enclosures of mathematical operations. These
interval enclosures may be not optimal floating-point intervals but in
most cases the error is no more than 1 ulp for each interval endpoint.
Interval2 is another simple OCaml interval
arithmetic library. It computes optimal floating-point intervals for
basic arithmetic operations. In some cases, it performs computations
with rational arithmetic. This library is slower than Interval1 but
it may be used in cases when optimal intervals are required (for
instance, when point intervals play an important role or when
discontinuous functions are considered).
See the docs directory.
See the tests directory.