{"id":2549,"date":"2013-03-06T06:09:42","date_gmt":"2013-03-06T06:09:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-the-picard-algorithm-for-ordinary-differential-equations-in-coq\/"},"modified":"2013-03-08T05:47:33","modified_gmt":"2013-03-08T05:47:33","slug":"resena-the-picard-algorithm-for-ordinary-differential-equations-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-the-picard-algorithm-for-ordinary-differential-equations-in-coq\/","title":{"rendered":"Rese\u00f1a: The Picard algorithm for ordinary differential equations in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado <a href=\"www.cs.ru.nl\/~spitters\/Picard.pdf\">The Picard algorithm for ordinary differential equations in Coq<\/a>.<\/p>\n<p>Sus autores son <a href=\"https:\/\/github.com\/EvgenyMakarov\">Evgeny Makarov<\/a> and <a href=\"http:\/\/www.cs.ru.nl\/~spitters\">Bas Spitters<\/a> (de la Universidad de Nimega, Pa\u00edses Bajos).<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nOrdinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindel\u00f6f 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\u00f6f 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.\n<\/p><\/blockquote>\n<p>Las teor\u00edas desarrolladas se encuentran <a href=\"https:\/\/github.com\/EvgenyMakarov\/corn\/tree\/master\/ode\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado The Picard algorithm for ordinary differential equations in Coq. Sus autores son Evgeny Makarov and Bas Spitters (de la Universidad de Nimega, Pa\u00edses Bajos). Su resumen es Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindel\u00f6f theorem&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,273,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2549"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2549"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2549\/revisions"}],"predecessor-version":[{"id":2678,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2549\/revisions\/2678"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2549"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2549"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2549"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}