{"id":2144,"date":"2012-08-23T06:36:43","date_gmt":"2012-08-23T06:36:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2144"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"a-refinement-based-approach-to-computational-algebra-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/a-refinement-based-approach-to-computational-algebra-in-coq\/","title":{"rendered":"Rese\u00f1a: A refinement-based approach to computational algebra in Coq"},"content":{"rendered":"<p>El lunes (13 de agosto de 2012) se present\u00f3 en el <a href=\"http:\/\/itp2012.cs.princeton.edu\">ITP 2012<\/a> (Interactive Theorem Proving) un trabajo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> titulado <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\/papers\/coqeal.pdf\">A refinement-based approach to computational algebra in Coq<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www-sop.inria.fr\/members\/Maxime.Denes\">Maxime D\u00e9n\u00e8s<\/a> (del <i>INRIA Sophia Antipolis, Francia<\/i>) y <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\">Anders M\u00f6rtberg<\/a> y <a href=\"http:\/\/www.cse.chalmers.se\/~siles\">Vincent Siles<\/a> (de la <i>Univ. de Gotemburgo, Suecia<\/i>).<\/p>\n<p>El resumen del trabajo es<\/p>\n<blockquote><p>\nWe describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd\u2019s fast matrix product, Karatsuba\u2019s polynomial multiplication, and the gcd of multivariate polynomials.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n en Coq se encuentra <a href=\"http:\/\/www-sop.inria.fr\/members\/Maxime.Denes\/coqeal\">aqu\u00ed<\/a>.<\/p>\n<p>Este trabajo es parte del proyecto <a href=\"http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ForMath\">ForMath: Formalisation of Mathematics<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El lunes (13 de agosto de 2012) se present\u00f3 en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado A refinement-based approach to computational algebra in Coq. Sus autores son Maxime D\u00e9n\u00e8s (del INRIA Sophia Antipolis, Francia) y Anders M\u00f6rtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia). El&#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\/2144"}],"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=2144"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2144\/revisions"}],"predecessor-version":[{"id":2789,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2144\/revisions\/2789"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2144"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2144"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2144"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}