{"id":4807,"date":"2015-03-19T07:27:18","date_gmt":"2015-03-19T06:27:18","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4807"},"modified":"2015-03-19T07:27:18","modified_gmt":"2015-03-19T06:27:18","slug":"resena-generalizing-a-mathematical-analysis-library-in-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-generalizing-a-mathematical-analysis-library-in-isabellehol\/","title":{"rendered":"Rese\u00f1a: Generalizing a mathematical analysis library in Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado <a href=\"http:\/\/bit.ly\/1F4Etws\">Generalizing a mathematical analysis library in Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.unirioja.es\/cu\/jearansa\">Jes\u00fas Aransay<\/a> y <a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\">Jose Divas\u00f3n<\/a> de la Universidad de la Rioja.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  The HOL Multivariate Analysis Library (HMA) of Isabelle\/HOL is focused on concrete types such as R, C and R n and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of HMA to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/nasaformalmethods.org\">NFM 2015<\/a> (<em>The 7th NASA Formal Methods Symposium<\/em>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Generalizing a mathematical analysis library in Isabelle\/HOL. Sus autores son Jes\u00fas Aransay y Jose Divas\u00f3n de la Universidad de la Rioja. Su resumen es The HOL Multivariate Analysis Library (HMA) of Isabelle\/HOL is focused on concrete types such as R, C and R n&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[144,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\/4807"}],"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=4807"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4807\/revisions"}],"predecessor-version":[{"id":4808,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4807\/revisions\/4808"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4807"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4807"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4807"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}