{"id":3393,"date":"2013-06-10T05:09:20","date_gmt":"2013-06-10T05:09:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3393"},"modified":"2013-06-10T05:09:20","modified_gmt":"2013-06-10T05:09:20","slug":"resena-certified-hlints-with-isabelleholcf-prelude","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-certified-hlints-with-isabelleholcf-prelude\/","title":{"rendered":"Rese\u00f1a: Certified HLints with Isabelle\/HOLCF-Prelude"},"content":{"rendered":"<p>Se ha publicado un trabajo de verificaci\u00f3n formal con <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle<\/a> sobre Haskell titulado <a href=\"http:\/\/arxiv.org\/pdf\/1306.1340v1\">Certified HLints with Isabelle\/HOLCF-Prelude<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/pp.ipd.kit.edu\/person.php?id=115\">Joachim Breitner<\/a>, <a href=\"http:\/\/www21.in.tum.de\/~huffman\/\">Brian Huffman<\/a>, <a href=\"http:\/\/community.haskell.org\/~ndm\/\">Neil Mitchell<\/a> y <a href=\"http:\/\/www.jaist.ac.jp\/~c-sterna\/\">Christian Sternagel<\/a>.<\/p>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/www.imn.htwk-leipzig.de\/HART2013\/\">HART 2013<\/a> (<i>\t1st International Workshop on Haskell And Rewriting Techniques<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present the <a href=\"http:\/\/sourceforge.net\/projects\/holcf-prelude\/\">HOLCF-Prelude<\/a>, a formalization of a large part of <a href=\"http:\/\/www.haskell.org\/onlinereport\/standard-prelude.html\">Haskell&#8217;s standard prelude<\/a> in <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/pubs\/jfp99.html\">Isabelle\/HOLCF<\/a>. Applying this formalization to the hints suggested by <a href=\"http:\/\/community.haskell.org\/~ndm\/hlint\/\">HLint<\/a> allows us to certify them formally.\n<\/p><\/blockquote>\n<p>El c\u00f3dido del HOLCF-Prelude se encuentra <a href=\"http:\/\/sourceforge.net\/p\/holcf-prelude\/code\/ci\/default\/tree\/\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un trabajo de verificaci\u00f3n formal con Isabelle sobre Haskell titulado Certified HLints with Isabelle\/HOLCF-Prelude. Sus autores son Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel. El trabajo se presentar\u00e1 en el HART 2013 ( 1st International Workshop on Haskell And Rewriting Techniques). Su resumen es We present the HOLCF-Prelude, a formalization&#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":[270,85,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\/3393"}],"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=3393"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3393\/revisions"}],"predecessor-version":[{"id":3394,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3393\/revisions\/3394"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3393"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3393"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3393"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}