{"id":3878,"date":"2013-12-03T07:49:20","date_gmt":"2013-12-03T06:49:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3878"},"modified":"2013-12-03T07:49:20","modified_gmt":"2013-12-03T06:49:20","slug":"refinements-for-free","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/refinements-for-free\/","title":{"rendered":"Refinements for free!"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre refinamientos de datos titulado <a href=\"http:\/\/www.maximedenes.fr\/download\/refinements.pdf\">Refinements for free!<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li><a href=\"http:\/\/perso.crans.org\/cohen\/\">Cyril Cohen<\/a> (de la <i>Univ. de Gotemburgo, Suecia<\/i>),\n<li><a href=\"http:\/\/www.maximedenes.fr\/\">Maxime D\u00e9n\u00e8s<\/a> (de la <i>Univ. de Pensilvania, EE.UU.<\/i>) y\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\/\">Anders M\u00f6rtberg<\/a> (de la <i>Univ. de Gotemburgo, Suecia<\/i>).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nFormal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures. Our design is general enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/cpp2013.forge.nicta.com.au\/\">CPP 2013<\/a> (<i>3rd International Conference on Certified Programs and Proofs<\/i>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre refinamientos de datos titulado Refinements for free!. Sus autores son Cyril Cohen (de la Univ. de Gotemburgo, Suecia), Maxime D\u00e9n\u00e8s (de la Univ. de Pensilvania, EE.UU.) y Anders M\u00f6rtberg (de la Univ. de Gotemburgo, Suecia). Su resumen es Formal verification of algorithms often requires&#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":[45,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\/3878"}],"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=3878"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3878\/revisions"}],"predecessor-version":[{"id":3879,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3878\/revisions\/3879"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3878"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3878"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3878"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}