Email Gateway (Aug 22 2022 at 21:03): Email Gateway (Aug 22 2022 at 21:03):From: Tobias Nipkow <nipkow@in.tum.de>
Interval Arithmetic on 32-bit Words
Brandon Bohrer
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.
https://www.isa-afp.org/entries/Interval_Arithmetic_Word32.html
Enjoy!
smime.p7s
Last updated: Apr 26 2024 at 16:20 UTC