Interval Arithmetic on 32-bit Words


Title: Interval Arithmetic on 32-bit Words
Author: Brandon Bohrer (bbohrer /at/ cs /dot/ cmu /dot/ edu)
Submission date: 2019-11-27
Abstract: 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.
  author  = {Brandon Bohrer},
  title   = {Interval Arithmetic on 32-bit Words},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2019,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Word_Lib
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.