{"id":2128,"date":"2012-08-16T06:13:46","date_gmt":"2012-08-16T06:13:46","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2128"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"resena-abstract-interpretation-of-annotated-commands","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-abstract-interpretation-of-annotated-commands\/","title":{"rendered":"Rese\u00f1a: Abstract interpretation of annotated commands"},"content":{"rendered":"<p>El lunes (13 de agosto de 2012) se present\u00f3 en el <a href=\"http:\/\/itp2012.cs.princeton.edu\">ITP 2012<\/a> (Interactive Theorem Proving) un trabajo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\">Isabelle<\/a> titulado <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/pubs\/itp12.pdf\">Abstract interpretation of annotated commands<\/a>. <\/p>\n<p>Su autor es <a href=\"http:\/\/www21.in.tum.de\/~nipkow\">Tobias Nipkow<\/a> (del <a href=\"http:\/\/www21.in.tum.de\">Theorem Proving Group<\/a> de la <a href=\"http:\/\/www.tu-muenchen.de\">Technische Universit\u00e4t M\u00fcnchen<\/a>).<\/p>\n<p>El resumen del trabajo es<\/p>\n<blockquote><p>\nThis paper formalises a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.\n<\/p><\/blockquote>\n<p>Las correspondientes teor\u00edas de Isabelle se encuentran <a href=\"http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-IMP\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El lunes (13 de agosto de 2012) se present\u00f3 en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle titulado Abstract interpretation of annotated commands. Su autor es Tobias Nipkow (del Theorem Proving Group de la Technische Universit\u00e4t M\u00fcnchen). El resumen del trabajo es This paper formalises a generic abstract interpreter&#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":[100],"tags":[85,273,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\/2128"}],"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=2128"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2128\/revisions"}],"predecessor-version":[{"id":2795,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2128\/revisions\/2795"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2128"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2128"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2128"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}