Plotting in a Formally Verified Way
This addresses accuracy issues in plotting for library designers in formal verification and mathematics, though it is incremental as it builds on existing Coq tools.
The paper tackled the problem of inaccurate function plots in computer algebra systems by defining correctness criteria and using the Coq proof assistant to generate formally verified plots via polynomial approximations, resulting in a tool integrated into the CoqInterval library.
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 using reliable polynomial approximations. This feature is provided as part of the CoqInterval library.