The Picard Algorithm for Ordinary Differential Equations in Coq

DOI10.1007/978-3-642-39634-2_34MaRDI QIDQ5327365zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

constructive mathematicsCoqexact real computationordinary differential equationstype classes

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to ordinary differential equations (34-04) Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations (34A12)

Recommendations

• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Taylor series solutions of explicit ODE's in a strongly typed algebra system
• Embedding of Systems of Affine Recurrence Equations in Coq
• A refinement-based approach to computational algebra in Coq
• Algorithmic methods for ordinary differential equations
• Partial derivative automata formalized in Coq
• Algorithmic Lie theory for solving ordinary differential equations
• scientific article; zbMATH DE number 2009905
• scientific article; zbMATH DE number 4123290

Cited in

(22)

• A verified ODE solver and the Lorenz attractor
• The flow of ODEs: formalization of variational equation and Poincaré map
• 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
• A Coq formalization of Lebesgue integration of nonnegative functions
• Formally verified approximations of definite integrals
• Formalization of real analysis: a survey of proof assistants and libraries
• Embedding of Systems of Affine Recurrence Equations in Coq
• Computable analysis and notions of continuity in \textsc{Coq}
• Constructive game logic
• Quantitative continuity and Computable Analysis in Coq
• Optimal control studies on age structured modeling of COVID-19 in presence of saturated medical treatment of Holling type III
• A formalization of metric spaces in HOL Light
• Refining constructive hybrid games
• A Coq formalization of Taylor models and power series for solving ordinary differential equations
• Mathematical modelling of the co-infection dynamics of soil-transmitted helminths and schistosomiasis with optimal control
• Computable analysis for extraction of certified programs and its applications
• Switched systems in Coq for modeling periodic controllers
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL
• C-CoRN
• Coq

This page was built for publication: The Picard Algorithm for Ordinary Differential Equations in Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327365)