{"id":2227,"date":"2012-10-15T05:07:14","date_gmt":"2012-10-15T05:07:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2227"},"modified":"2013-03-08T05:44:48","modified_gmt":"2013-03-08T05:44:48","slug":"resena-proof-pearl-a-mechanized-proof-of-ghc%e2%80%99s-mergesort","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-proof-pearl-a-mechanized-proof-of-ghc%e2%80%99s-mergesort\/","title":{"rendered":"Rese\u00f1a: Proof pearl &#8211; A mechanized proof of GHC\u2019s mergesort"},"content":{"rendered":"<p>Se publicado un art\u00edculo de verificaci\u00f3n en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/\">Iabelle\/HOL<\/a> titulado <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\/publications\/S-JAR12.pdf\">Proof pearl &#8211; A mechanized proof of GHC\u2019s mergesort<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\/index.php\">Christian Sternagel<\/a> (de la Univ. de la Univ. de Insbruck).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present our Isabelle\/HOL formalization of GHC\u2019s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.\n<\/p><\/blockquote>\n<p>La librer\u00eda est\u00e1ndard de <a href=\"http:\/\/www.haskell.org\/ghc\/\">GHC (The Glasgow Haskell Compiler)<\/a> tiene un <a href=\"http:\/\/www.haskell.org\/ghc\/docs\/7.0-latest\/html\/libraries\/base-4.3.1.0\/src\/Data-List.html#sort\">algoritmo de ordenaci\u00f3n<\/a>, que es una variante de la ordenaci\u00f3n por mezcla. El objetivo del trabajo es la verificaci\u00f3n de dicho algortimo en Isabelle\/HOL, demostrando su correcci\u00f3n y estabilidad.<\/p>\n<p>La principal caracter\u00edstica de este trabajo es la verificaci\u00f3n de programas eficientes. El m\u00e9todo empleado tiene tres pasos:<\/p>\n<ol>\n<li>formalizar variantes del algoritmo que faciliten la demostraci\u00f3n y probar todas las propiedades deseadas;\n<li>formalizar variantes eficientes del algoritmo y probar su equivalencia y\n<li>usar la <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/dist\/Isabelle2012\/doc\/codegen.pdf\">generaci\u00f3n de c\u00f3digo<\/a> y obtener un programa eficiente del que se tiene garant\u00eda que satisface todas las propiedades que se probaron en la formalizaci\u00f3n inicial.\n<\/ol>\n<p>La formalizaci\u00f3n es peque\u00f1a (menos de 400 l\u00edneas de c\u00f3digo) y la mayor\u00eda de las demostraciones son autom\u00e1ticas. Este \u00e9xito se basa en dos principios: la generalizaci\u00f3n de los conceptos y la definici\u00f3n de esquemas de inducci\u00f3n.<\/p>\n<p>El c\u00f3digo en Isabelle\/HOL de la teor\u00eda correspondiente al trabajo se encuentra en <a href=\"http:\/\/afp.sourceforge.net\/entries\/Efficient-Mergesort.shtml\">The Archive of Formal Proofs.<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se publicado un art\u00edculo de verificaci\u00f3n en Iabelle\/HOL titulado Proof pearl &#8211; A mechanized proof of GHC\u2019s mergesort. Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck). Su resumen es We present our Isabelle\/HOL formalization of GHC\u2019s sorting algorithm for lists, proving its correctness and stability. This constitutes another example 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":[89,135,270,144,285,275],"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\/2227"}],"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=2227"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2227\/revisions"}],"predecessor-version":[{"id":2655,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2227\/revisions\/2655"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2227"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2227"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2227"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}