@inproceedings{25e77b2706f346238cd4c917750f9f34,
title = "The Picard algorithm for ordinary differential equations in Coq",
abstract = "Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindel{\"o}f theorem is the first fundamental theorem in the theory of ODEs. It allows one to solve differential equations numerically. We provide a constructive development of the Picard-Lindel{\"o}f theorem which includes a program together with sufficient conditions for its correctness. The proof/program is written in the Coq proof assistant and uses the implementation of efficient real numbers from the CoRN library and the MathClasses library. Our proof makes heavy use of operators and functionals, functions on spaces of functions. This is faithful to the usual mathematical description, but a novel level of abstraction for certified exact real computation.",
keywords = "Constructive mathematics, Coq, Exact real computation, Ordinary Differential Equations, Type classes",
author = "Evgeny Makarov and Bas Spitters",
year = "2013",
month = aug,
day = "28",
doi = "10.1007/978-3-642-39634-2_34",
language = "English",
isbn = "9783642396335",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "463--468",
booktitle = "Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings",
note = "4th International Conference on Interactive Theorem Proving, ITP 2013 ; Conference date: 22-07-2013 Through 26-07-2013",
}