A Parameterized Floating-Point Formalizaton in HOL Light | Zendy

Charles Jacobsen | Zendy; Alexey Solovyev | Zendy; Ganesh Gopalakrishnan | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Parameterized Floating-Point Formalizaton in HOL Light

Author(s) -

Charles Jacobsen,

Alexey Solovyev,

Ganesh Gopalakrishnan

Publication year - 2015

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2015.10.010

Subject(s) - hol , rounding , ieee floating point , floating point , parameterized complexity , computer science , correctness , mathematical proof , algorithm , fixed point , point (geometry) , discrete mathematics , single precision floating point format , set (abstract data type) , mathematics , arithmetic , programming language , geometry , mathematical analysis , operating system

We present a new, open-source formalization of fixed and floating-point numbers for arbitrary radix and precision that is now part of the HOL Light distribution [John Harrison. HOL Light: A tutorial introduction. In Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996]. We prove correctness and error bounds for the four different rounding modes, and formalize a subset of the IEEE 754 [IEEE standard for floating point arithmetic. IEEE Std. 754-2008, 2008] standard by gluing together a set of fixed-point and floating-point numbers to represent the subnormals and normals. In our floating-point proofs, we treat phases of floating-point numbers as copies of fixed-point numbers of varying precision so that we can reuse fixed-point rounding theorems

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research