{"id":4366,"date":"2014-07-10T08:01:52","date_gmt":"2014-07-10T06:01:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4366"},"modified":"2014-07-10T08:02:50","modified_gmt":"2014-07-10T06:02:50","slug":"resena-truly-modular-codatatypes-for-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-truly-modular-codatatypes-for-isabellehol\/","title":{"rendered":"Rese\u00f1a: Truly modular (co)datatypes for Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> sobre automatizaci\u00f3n del razonamiento titulado <a href=\"http:\/\/bit.ly\/1j7IMgM\">Truly modular (co)datatypes for Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www21.in.tum.de\/~blanchet\">Jasmin Christian Blanchette<\/a> (de la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania), <\/li>\n<li><a href=\"http:\/\/www.in.tum.de\/~hoelzl\">Johannes H\u00f6lzl<\/a> (de la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania), <\/li>\n<li><a href=\"http:\/\/www.infsec.ethz.ch\/people\/andreloc\">Andreas Lochbihler<\/a> (del <em>ETH Zurich<\/em>, Suiza), <\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~panny\">Lorenz Panny<\/a> (de la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania), <\/li>\n<li><a href=\"http:\/\/www4.in.tum.de\/~popescua\">Andrei Popescu<\/a> (de la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania) y <\/li>\n<li><a href=\"http:\/\/www21.in.tum.de\/~traytel\">Dmitriy Traytel<\/a> (de la <em>Technische Universit\u00e4t M\u00fcnchen<\/em>, Alemania).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>&#8220;We extended Isabelle\/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion\u2013corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle\u2019s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.&#8221;<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el lunes 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<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/www21.in.tum.de\/~blanchet\/codata_impl.tar.gz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre automatizaci\u00f3n del razonamiento titulado Truly modular (co)datatypes for Isabelle\/HOL. Sus autores son Jasmin Christian Blanchette (de la Technische Universit\u00e4t M\u00fcnchen, Alemania), Johannes H\u00f6lzl (de la Technische Universit\u00e4t M\u00fcnchen, Alemania), Andreas Lochbihler (del ETH Zurich, Suiza), Lorenz Panny (de la Technische Universit\u00e4t M\u00fcnchen, Alemania), Andrei&#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\/4366"}],"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=4366"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4366\/revisions"}],"predecessor-version":[{"id":4369,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4366\/revisions\/4369"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4366"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4366"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4366"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}