### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Interval_Arithmetic_Word32

- Interval_Word32
- Finite_String
- Interpreter

### Depends on

- Finite Machine Word Library

### Auto-related entries

- Continued Fractions
- Factorization of Polynomials with Algebraic Coefficients

## Cite

×

Interval_Arithmetic_Word32-AFP

    @article{Interval_Arithmetic_Word32-AFP,
      author  = {Rose Bohrer},
      title   = {Interval Arithmetic on 32-bit Words},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Interval_Arithmetic_Word32.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Nov 28, 2019 : Isabelle2019