Plotting in a Formally Verified Way

Guillaume Melquiond

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.

In José Proença and Andrei Paskevich: Proceedings of the 6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Held online, 24-25th May 2021, Electronic Proceedings in Theoretical Computer Science 338, pp. 39–45.
Published: 6th August 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: