Skip to content

Fp/ieee

Arthur Correnson requested to merge fp/ieee into master

This merge request propose a partial integration of floating-points intervals based on a Coq formalization (Farith2). For now, the OCaml extraction of the Coq modules is inefficient and incompatible with the valuation modules for FP (i.e. : Farith).

To fix this issue, we provides a tinny compatibility layer between Farith's & Farith2's floating-points. It is planed to merge Farith & Farith2 as a unified package providing a verified implementation of both FP numbers and FP domains

Merge request reports