{"id":6937,"date":"2020-01-12T12:06:55","date_gmt":"2020-01-12T11:06:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6937"},"modified":"2020-01-12T12:06:55","modified_gmt":"2020-01-12T11:06:55","slug":"resena-proof-pearl-braun-trees","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-proof-pearl-braun-trees\/","title":{"rendered":"Rese\u00f1a: &#8220;Proof pearl: Braun trees&#8221;"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre algor\u00edtmica titulado <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/pubs\/cpp20.pdf\">Proof pearl: Braun trees<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www21.in.tum.de\/~nipkow\">Tobias Nipkow<\/a> (del <a href=\"http:\/\/www21.in.tum.de\/\">Theorem Proving Group<\/a> en la <i>Technische Universit\u00e4t M\u00fcnchen<\/i>, Alemania) y<\/li>\n<li><a href=\"https:\/\/popl20.sigplan.org\/profile\/thomassewell1\">Thomas Sewell<\/a> (del <a href=\"https:\/\/www.chalmers.se\/en\/departments\/cse\/organisation\/fm\/Pages\/default.aspx\">Formal Methods Group<\/a> en la <i>Chalmers University of Technology<\/i>, Suecia).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>Braun trees are functional data structures for implementing extensible arrays and priority queues (and sorting functions based on the latter) efficiently. Some well-known functions on Braun trees have not yet been verified, including especially Okasaki\u2019s linear time conversion from lists to Braun trees. We supply the missing proofs and verify all of these algorithms in Isabelle, including non-obvious time complexity claims. In particular we provide the first linear-time conversion from Braun trees to lists. We also state and verify a new characterization of Braun trees as the trees t whose index set is the interval {1,\u2026, size of t}.<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"https:\/\/popl20.sigplan.org\/\">POPL 2020 (47th ACM SIGPLAN Symposium on Principles of Programming Languages)<\/a> el pr\u00f3ximo 20 de enero.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra en <a href=\"https:\/\/www.isa-afp.org\/entries\/Priority_Queue_Braun.html\">AFP<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre algor\u00edtmica titulado Proof pearl: Braun trees. Sus autores son Tobias Nipkow (del Theorem Proving Group en la Technische Universit\u00e4t M\u00fcnchen, Alemania) y Thomas Sewell (del Formal Methods Group en la Chalmers University of Technology, Suecia). Su resumen es Braun trees are functional data structures&#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":[],"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\/6937"}],"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=6937"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6937\/revisions"}],"predecessor-version":[{"id":6938,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6937\/revisions\/6938"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6937"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6937"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6937"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}