{"id":4739,"date":"2015-01-26T08:13:03","date_gmt":"2015-01-26T07:13:03","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4739"},"modified":"2015-01-26T08:13:03","modified_gmt":"2015-01-26T07:13:03","slug":"resena-hocore-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-hocore-in-coq\/","title":{"rendered":"Rese\u00f1a: HOCore in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado <a href=\"http:\/\/bit.ly\/1yUeaFJ\">HOCore in Coq<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"mailto:mescarra@gmail.com\">Mart\u00edn Escarr\u00e1<\/a>(de la Universidad Nacional de Rosario, Argentina),<\/li>\n<li><a href=\"https:\/\/sites.google.com\/site\/petarmaksimovic1981\/home\">Maksimovi\u0107 Petar<\/a> (del grupo <a href=\"http:\/\/www.irisa.fr\/celtique\">Celtique<\/a> en el INRIA Rennes) y<\/li>\n<li><a href=\"http:\/\/www.irisa.fr\/celtique\/aschmitt\">Alan Schmitt<\/a> (del grupo <a href=\"http:\/\/www.irisa.fr\/celtique\">Celtique<\/a> en el INRIA Rennes) <\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We consider a recent publication on higher-order process calculi and describe how its results are formalized in the Coq proof assistant. We also highlight some important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration, and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en las <a href=\"http:\/\/jfla.inria.fr\/2015\">Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2015)<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/www.irisa.fr\/celtique\/aschmitt\/research\/hocore\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado HOCore in Coq. Sus autores son Mart\u00edn Escarr\u00e1(de la Universidad Nacional de Rosario, Argentina), Maksimovi\u0107 Petar (del grupo Celtique en el INRIA Rennes) y Alan Schmitt (del grupo Celtique en el INRIA Rennes) Su resumen es We consider a recent publication on higher-order process&#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":[45,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\/4739"}],"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=4739"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4739\/revisions"}],"predecessor-version":[{"id":4740,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4739\/revisions\/4740"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4739"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4739"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4739"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}