Published July 22, 2017
| Version v1
Conference paper
Formal correctness of comparison algorithms between binary64 and decimal64 floating-point numbers
Contributors
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.
Abstract
International audienceAdditional details
Identifiers
- URL
- https://hal.science/hal-01512294
- URN
- urn:oai:HAL:hal-01512294v1
Origin repository
- Origin repository
- UNICA