Skip to Main content Skip to Navigation
Preprints, Working 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Guillaume Melquiond <>
Submitted on : Friday, March 12, 2021 - 6:18:58 PM
Last modification on : Tuesday, April 13, 2021 - 9:36:42 AM


Files produced by the author(s)


  • HAL Id : hal-03168208, version 1


Guillaume Melquiond. Plotting in a Formally Verified Way. 2021. ⟨hal-03168208⟩



Record views


Files downloads