Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers

Others:: École normale supérieure - Lyon (ENS Lyon); Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS); Arithmetic and Computing (ARIC) ; Inria Grenoble - Rhône-Alpes ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS); Centre National de la Recherche Scientifique (CNRS); Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria); ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014)

Description

We present a full Coq formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers.

International audience