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.
BibTeX:
@article{Interval_Arithmetic_Word32-AFP,
  author  = {Brandon Bohrer},
  title   = {Interval Arithmetic on 32-bit Words},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2019,
  note    = {\url{https://isa-afp.org/entries/Interval_Arithmetic_Word32.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Word_Lib