Rigorous polynomial approximation using taylor models in Coq

摘要: One of the most common and practical ways representing a real function on machines is by using polynomial approximation. It then important to properly handle error introduced such an The purpose this work offer guaranteed bounds for specific kind rigorous approximation called Taylor model. We carry out in Coq proof assistant, with special focus genericity efficiency our implementation. give abstract interface approximations, parameterized type coefficients implementation polynomials, we instantiate case models interval coefficients, while providing all machinery computing them. compare performances those Sollya tool, which contains written C. This milestone long-term goal fully formally proved efficient models.