{"id":3189,"date":"2013-04-08T04:53:42","date_gmt":"2013-04-08T04:53:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3189"},"modified":"2013-04-08T04:53:42","modified_gmt":"2013-04-08T04:53:42","slug":"resena-data-refinement-in-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-data-refinement-in-isabellehol\/","title":{"rendered":"Rese\u00f1a: Data refinement in Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre automatizaci\u00f3n del razonamiento en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/isabelle.in.tum.de\/~haftmann\/pdf\/data_refinement_haftmann_kuncar_krauss_nipkow.pdf\">Data refinement in Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/isabelle.in.tum.de\/~haftmann\">Florian Haftmann<\/a>, <a href=\"http:\/\/www21.in.tum.de\/~krauss\">Alexander Krauss<\/a>, <a href=\"http:\/\/www21.in.tum.de\/~kuncar\">Ond\u0159ej Kun\u010dar<\/a> y <a href=\"http:\/\/www21.in.tum.de\/~nipkow\">Tobias Nipkow<\/a> (de la Universidad T\u00e9cnica de Munich). <\/p>\n<p>El trabajo se presentar\u00e1 en julio en el <a href=\"http:\/\/itp2013.inria.fr\">ITP 2013<\/a> (4th Conference on<br \/>\nInteractive Theorem Proving).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe paper shows how the code generator of Isabelle\/HOL supports data refinement, i.e., providing efficient code for operations on abstract types, e.g., sets or numbers. This allows all tools that employ code generation, e.g., Quickcheck or proof by evaluation, to compute with these abstract types. At the core is an extension of the code generator to deal with data type invariants. In order to automate the process of setting up specific data refinements, two packages for transferring definitions and theorems between types are exploited.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre automatizaci\u00f3n del razonamiento en Isabelle\/HOL titulado Data refinement in Isabelle\/HOL. Sus autores son Florian Haftmann, Alexander Krauss, Ond\u0159ej Kun\u010dar y Tobias Nipkow (de la Universidad T\u00e9cnica de Munich). El trabajo se presentar\u00e1 en julio en el ITP 2013 (4th Conference on Interactive Theorem Proving). Su resumen es The paper&#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":[1],"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\/3189"}],"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=3189"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3189\/revisions"}],"predecessor-version":[{"id":3190,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3189\/revisions\/3190"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3189"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3189"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3189"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}