Translating Floating-Point to Bit-Vector Operations in Isabelle/HOL

Calculations with real numbers are commonly approximated by floating-point arithmetic in computers. A floating-point number is represented by a fixed number of bits. Arithmetic operations, such as addition or multiplication, return a rounded result when the precise result of the operation cannot be represented as a floating-point number with the given (limited) precision.

It is often important to reason about floating-point arithmetic; for instance, to show the correctness of numerical algorithms. A common approach to reason about floating-point arithmetic automatically is to translate n-bit floating-point numbers into bit vectors of length n: i.e., to reason about the bit representation of floating-point numbers. Arithmetic operations on floating-point numbers then correspond to certain bit operations over these vectors. The software library SymFPU implements such a translation.

The goal of this project is to implement a translation of floating-point arithmetic into bit vectors for the interactive proof assistant Isabelle. In contrast to SymFPU, which simply computes the result of the translation, this implementation will also need to produce a proof (in Isabelle) that the generated bit-vector problem is equivalent to the original floating-point problem. The translation should eventually become part of the Isabelle system. Therefore, it must be implemented in Standard ML.

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:
Standard ML, Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Functional programming, floating-point arithmetic, first-order logic
Tjark Weber

Last modified: 2023-11-05