{"id":2130,"date":"2012-08-17T05:46:26","date_gmt":"2012-08-17T05:46:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2130"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"construction-of-real-algebraic-numbers-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/construction-of-real-algebraic-numbers-in-coq\/","title":{"rendered":"Rese\u00f1a: Construction of real algebraic numbers 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:\/\/perso.crans.org\/cohen\/papers\/realalg.pdf\">Construction of real algebraic numbers in Coq<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/perso.crans.org\/cohen\">Cyril Cohen<\/a> (de la \u00c9cole Polytechnique (Palaiseau, Francia)).<\/p>\n<p>El resumen del trabajo es<\/p>\n<blockquote><p>\nThis paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n en Coq se encuentra en <a href=\"http:\/\/perso.crans.org\/cohen\/work\/realalg\/code\/realalg.tgz\">realalg.tgz<\/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 Construction of real algebraic numbers in Coq. Su autor es Cyril Cohen (de la \u00c9cole Polytechnique (Palaiseau, Francia)). El resumen del trabajo es This paper shows a construction in Coq of&#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\/2130"}],"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=2130"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2130\/revisions"}],"predecessor-version":[{"id":2794,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2130\/revisions\/2794"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2130"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2130"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2130"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}