Floating-point arithmetic is often implemented in dedicated hardware accelerators, but can also be implemented in software. The interactive proof assistant Isabelle offers an implementation of floating-point arithmetic in formal logic. This facilitates reasoning about the behavior of floating-point operations; for instance, to prove that x+y = y+x for all floating-point numbers x and y (where + denotes floating-point addition).
Isabelle's floating-point implementation is well-suited for reasoning about floating-point arithmetic, but the formal definitions are not directly executable: performinmg calculations with concrete numbers - for instance, computing the result of 3.14159 + 2.71828 - requires significant assistance from the user. The goal of this project is to provide automation for floating-point calculations in Isabelle; for instance, by porting the existing automation for floating-point calculations that has been developed for the HOL4 proof assistant.
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.