I den här artikeln presenterar vi ett allmänt bibliotek för att resonera om flyttalnummer inom Coq-systemet. De flesta av bibliotekets resultat är bevisade för ett godtyckligt flyttalformat och en godtycklig bas. Särskild vikt har lagts vid att bevisa egenskaper för exakt beräkning, d.v.s. Datorer utan avrundningsfel.
Mer nyligen, Daumas et al. REF har presenterat ett generiskt bibliotek för resonemang om flyttalstal inom Coq-systemet.
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing
{'venue': 'TPHOLs', 'journal': None, 'mag_field_of_study': ['Computer Science']}