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{http://isa-afp.org/entries/Interval_Arithmetic_Word32.html}, 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.