HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Plotting in a Formally Verified Way

Guillaume Melquiond 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs that are guaranteed to be correct, by using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.
Complete list of metadata

https://hal.inria.fr/hal-03168208
Contributor : Guillaume Melquiond Connect in order to contact the contributor
Submitted on : Sunday, May 2, 2021 - 8:06:22 PM
Last modification on : Friday, February 4, 2022 - 3:08:33 AM

File

article.pdf
Files produced by the author(s)

Identifiers

Citation

Guillaume Melquiond. Plotting in a Formally Verified Way. Proceedings of the 6th Workshop on Formal Integrated Development Environment, May 2021, Online, United States. pp.39-45, ⟨10.4204/EPTCS.338.6⟩. ⟨hal-03168208v2⟩

Share

Metrics

Record views

111

Files downloads

405