Interval Arithmetic on 32-Bit Words

Rose Bohrer 📧

November 27, 2019

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Interval_Arithmetic implements conservative interval arithmetic computations, then uses this interval arithmetic to implement a simple programming language where all terms have 32-bit signed word values, with explicit infinities for terms outside the representable bounds. Our target use case is interpreters for languages that must have a well-understood low-level behavior. We include a formalization of bounded-length strings which are used for the identifiers of our language. Bounded-length identifiers are useful in some applications, for example the Differential_Dynamic_Logic article, where a Euclidean space indexed by identifiers demands that identifiers are finitely many.


BSD License


Session Interval_Arithmetic_Word32