{"id":4362,"date":"2014-07-09T09:20:39","date_gmt":"2014-07-09T07:20:39","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4362"},"modified":"2014-07-09T09:22:49","modified_gmt":"2014-07-09T07:22:49","slug":"resena-recursive-functions-on-lazy-lists-via-domains-and-topologies","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-recursive-functions-on-lazy-lists-via-domains-and-topologies\/","title":{"rendered":"Rese\u00f1a: Recursive functions on lazy lists via domains and topologies"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> <a href=\"http:\/\/bit.ly\/1j7IyX7\">Recursive functions on lazy lists via domains and topologies<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.infsec.ethz.ch\/people\/andreloc\">Andreas Lochbihler<\/a> (del <em>Institute of Information Security, ETH Zurich<\/em>) y<\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~hoelzl\">Johannes H\u00f6lzl<\/a> (del <em>Institut f\u00fcr Informatik, TU M\u00fcunchen<\/em>).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>The usual definition facilities in theorem provers cannot handle all recursive functions on codatatypes; the filter function on lazy lists is a prime counterexample. We present two new ways of directly defining functions like filter by exploiting their dual nature as producers and consumers. Borrowing from domain theory and topology, we define them as a least fixpoint (producer view) and as a continuous extension (consumer view). Both constructions yield proof principles that allow elegant proofs.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el lune 14 de julio en el <a href=\"http:\/\/www.cs.uwyo.edu\/~ruben\/itp-2014\">ITP 2014<\/a> (<em>5th Conference on Interactive Theorem Proving<\/em>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL Recursive functions on lazy lists via domains and topologies. Sus autores son Andreas Lochbihler (del Institute of Information Security, ETH Zurich) y Johannes H\u00f6lzl (del Institut f\u00fcr Informatik, TU M\u00fcunchen). Su resumen es The usual definition facilities in theorem provers cannot handle all recursive functions&#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":[229,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\/4362"}],"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=4362"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4362\/revisions"}],"predecessor-version":[{"id":4365,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4362\/revisions\/4365"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4362"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4362"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4362"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}