The Picard Algorithm for Ordinary Differential Equations in Coq
From MaRDI portal
Publication:5327365
DOI10.1007/978-3-642-39634-2_34zbMath1317.68222OpenAlexW69146909MaRDI QIDQ5327365
Evgeniĭ Olegovich Makarov, Bas Spitters
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_34
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Constructive Game Logic ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ A verified ODE solver and the Lorenz attractor ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Unnamed Item ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Formally verified approximations of definite integrals ⋮ Quantitative continuity and Computable Analysis in Coq ⋮ A formalization of metric spaces in HOL Light ⋮ Formally Verified Approximations of Definite Integrals ⋮ Time optimal control studies on COVID-19 incorporating adverse events of the antiviral drugs ⋮ Constructive hybrid games ⋮ Age structured mathematical modeling studies on COVID-19 with respect to combined vaccination and medical treatment strategies
Uses Software
This page was built for publication: The Picard Algorithm for Ordinary Differential Equations in Coq
