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.