{"id":3414,"date":"2013-06-22T09:41:15","date_gmt":"2013-06-22T09:41:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3414"},"modified":"2013-06-22T09:42:23","modified_gmt":"2013-06-22T09:42:23","slug":"resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials\/","title":{"rendered":"Rese\u00f1a: &#8220;Certified symbolic manipulation: Bivariate simplicial polynomials&#8221;"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en <a href=\"http:\/\/www.cs.utexas.edu\/~moore\/acl2\">ACL2<\/a> titulado <a href=\"http:\/\/wiki.portal.chalmers.se\/cse\/uploads\/ForMath\/issac17p-martin\">Certified symbolic manipulation: Bivariate simplicial polynomials<\/a>.<\/p>\n<p>Sus autores son <a href=\"https:\/\/esus.unirioja.es\/psycotrip\/index.php?op=miembro&#038;miembro=0005\">Laureano Lamb\u00e1n<\/a>, <a href=\"https:\/\/www.glc.us.es\/fmartin\">Francisco Jes\u00fas Mart\u00edn Mateos<\/a>, <a href=\"https:\/\/esus.unirioja.es\/psycotrip\/index.php?op=miembro&#038;miembro=0001\">Julio Rubio<\/a> y <a href=\"http:\/\/www.cs.us.es\/~jruiz\">Jos\u00e9 Luis Ruiz Reina<\/a>. <\/p>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/www.issac-symposium.org\/2013\">ISSAC 2013<\/a> (<i>38th International Symposium on Symbolic and Algebraic Computation<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nCertified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In  this paper, we focus on algebraic algorithms implemented in the proof assistant ACL2, which allows us to verify correctness in the same programming environment. The case study is that of <i>bivariate simplicial polynomials<\/i>, a data structure used to help the proof of properties in Simplicial Topology. Simplicial polynomials can be computationally interpreted  in two ways. As symbolic expressions, they can be handled  algorithmically, increasing the automation in ACL2 proofs. As representations of functional operators, they help proving  properties of categorical morphisms. As an application of  this second view, we present the definition in ACL2 of some  morphisms involved in the Eilenberg-Zilber reduction, a central part of the <a href=\"http:\/\/www-fourier.ujf-grenoble.fr\/~sergerar\/Kenzo\/\">Kenzo<\/a> computer algebra system. We have  proved the ACL2 implementations are correct and tested  that they get the same results as Kenzo does.\n<\/p><\/blockquote>\n<p>El c\u00f3digo ACL2 de la formalizaci\u00f3n del teorema de Eilenberg-Zilber se encuentra <a href=\"https:\/\/www.glc.us.es\/fmartin\/simplicial-topology\/eilenberg-zilber-theorem\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en ACL2 titulado Certified symbolic manipulation: Bivariate simplicial polynomials. Sus autores son Laureano Lamb\u00e1n, Francisco Jes\u00fas Mart\u00edn Mateos, Julio Rubio y Jos\u00e9 Luis Ruiz Reina. El trabajo se presentar\u00e1 en el ISSAC 2013 (38th International Symposium on Symbolic and Algebraic Computation). Su resumen es Certified symbolic manipulation&#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":[1],"tags":[49,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\/3414"}],"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=3414"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3414\/revisions"}],"predecessor-version":[{"id":3416,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3414\/revisions\/3416"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3414"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3414"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3414"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}