{"id":4999,"date":"2015-09-03T06:58:52","date_gmt":"2015-09-03T04:58:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4999"},"modified":"2015-09-03T06:58:52","modified_gmt":"2015-09-03T04:58:52","slug":"resena-stream-fusion-for-isabelles-code-generator","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-stream-fusion-for-isabelles-code-generator\/","title":{"rendered":"Rese\u00f1a: Stream fusion for Isabelle\u2019s code generator"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> <a href=\"http:\/\/www.infsec.ethz.ch\/content\/dam\/ethz\/special-interest\/infk\/inst-infsec\/information-security-group-dam\/people\/andreloc\/lochbihler2015itp.pdf\">Stream fusion for Isabelle\u2019s code generator<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.infsec.ethz.ch\/people\/andreloc.html\">Andreas Lochbihler<\/a> y Alexandra Maximova (del <a href=\"http:\/\/www.infsec.ethz.ch\/the-group.html\">Information Security Group<\/a> en la <a href=\"http:\/\/bit.ly\/1fWnou5\">Escuela Polit\u00e9cnica Federal de Z\u00farich<\/a>, Suiza).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle\/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.\n<\/p><\/blockquote>\n<p>Su contenido es un resumen de la tesis de M\u00e1ster <a href=\"http:\/\/www.infsec.ethz.ch\/education\/studentProjects\/former\/maximova.html\">Stream Fusion for Isabelle\u2019s Code Generator<\/a> realizada por Alexandra Maximova y dirigida por Andreas Lochbihler.<\/p>\n<p>El trabajo se present\u00f3 el 25 de agosto en el <a href=\"http:\/\/www.inf.kcl.ac.uk\/staff\/urbanc\/itp-2015\">ITP 2015<\/a> (<em>The 6th conference on Interactive Theorem Proving<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"http:\/\/afp.sourceforge.net\/browser_info\/current\/AFP\/Stream_Fusion_Code\/index.html\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento formalizado en Isabelle\/HOL Stream fusion for Isabelle\u2019s code generator. Sus autores son Andreas Lochbihler y Alexandra Maximova (del Information Security Group en la Escuela Polit\u00e9cnica Federal de Z\u00farich, Suiza). Su resumen es Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite&#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":[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\/4999"}],"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=4999"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4999\/revisions"}],"predecessor-version":[{"id":5000,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4999\/revisions\/5000"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4999"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4999"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4999"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}