Bachelor’s/Master’s Thesis
The Isabelle theorem prover can prove variable-free arithmetic statements automatically, for example arctan 1.5 < 1. The proof procedure uses Taylor polynomials and interval arithmetic. It should now be extended in the following directions:
Add further operations (in particular further trigonometric ones but also integrals) and extend it from real to complex numbers. This (or some subset of it) is appropriate for a bachelor’s thesis.
Currently all computations use software floating point numbers that are based on a software implementation of arbitrary precision integer arithmetic. The topic of this master’s thesis is to replace the software floats by hardware floats.
The work involves both programming and proving in Isabelle/HOL. In the case of the hardware floats this means proving the correctness of all algorithms with respect to the IEEE floating point specification. The latter has already been formalized in Isabelle.
Prerequisites:
Familiarity with Isabelle/HOL and floating point numbers
Supervisor:
Prof. Tobias Nipkow