{"id":3383,"date":"2013-05-30T05:47:42","date_gmt":"2013-05-30T05:47:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3383"},"modified":"2013-05-30T05:47:42","modified_gmt":"2013-05-30T05:47:42","slug":"resena-automatic-data-refinement","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-automatic-data-refinement\/","title":{"rendered":"Rese\u00f1a: Automatic data refinement"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www21.in.tum.de\/~lammich\/pub\/autoref.pdf\">Automatic data refinement<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www21.in.tum.de\/~lammich\">Peter Lammich<\/a> (de la Universidad T\u00e9cnica de Munich).<\/p>\n<p>El trabajo se presentar\u00e1 en julio en la <a href=\"http:\/\/itp2013.inria.fr\/\">ITP 2013<\/a> (<i>4th Conference on<br \/>\nInteractive Theorem Proving<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present the <a href=\"https:\/\/www21.in.tum.de\/~lammich\/autoref\/index.shtml\">Autoref tool<\/a> for Isabelle\/HOL, which automatically refines algorithms specified over abstract concepts like maps and sets to algorithms over concrete implementations like red-black-trees, and produces a refinement theorem. It is based on ideas borrowed from relational parametricity due to Reynolds and Wadler.<\/p>\n<p>The tool allows for rapid prototyping of verified, executable algorithms. Moreover, it can be configured to fine-tune the result to the user&#8217;s needs. Our tool is able to automatically instantiate generic algorithms, which greatly simplifies the implementation of executable data structures.<\/p>\n<p>Thanks to its integration with the Isabelle Refinement Framework and the Isabelle Collection Framework, Autoref can be used as a backend to a stepwise refinement based development approach, having access to a rich library of verified data structures. We have evaluated the tool by synthesizing efficiently executable refinements for some complex algorithms, as well as by implementing a library of generic algorithms for maps and sets.\n<\/p><\/blockquote>\n<p>La implementaci\u00f3n de Autoref, junto con algunos casos de estudio, se encuentra <a href=\"https:\/\/www21.in.tum.de\/~lammich\/autoref\/index.shtml\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en Isabelle\/HOL titulado Automatic data refinement. Su autor es Peter Lammich (de la Universidad T\u00e9cnica de Munich). El trabajo se presentar\u00e1 en julio en la ITP 2013 (4th Conference on Interactive Theorem Proving). Su resumen es We present the Autoref tool for Isabelle\/HOL, which automatically refines&#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":[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\/3383"}],"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=3383"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3383\/revisions"}],"predecessor-version":[{"id":3384,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3383\/revisions\/3384"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3383"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3383"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3383"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}