{"id":5023,"date":"2015-09-15T07:21:42","date_gmt":"2015-09-15T05:21:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5023"},"modified":"2015-09-15T07:21:42","modified_gmt":"2015-09-15T05:21:42","slug":"resena-deriving-comparators-and-show-functions-in-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-deriving-comparators-and-show-functions-in-isabellehol\/","title":{"rendered":"Rese\u00f1a: Deriving comparators and show functions in Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/thiemann\/paper\/ITP15Deriving.pdf\">Deriving comparators and show functions in Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\">Christian Sternagel<\/a> y <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/thiemann\">Ren\u00e9 Thiemann<\/a> (del <a href=\"http:\/\/cl-informatik.uibk.ac.at\">Computational Logic Research Group<\/a> en la <a href=\"http:\/\/bit.ly\/1ELGKOo\">Universidad de Innsbruck<\/a>, Austria).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We present an Isabelle\/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.<\/p>\n<p>  In contrast to similar mechanisms, like Haskell\u2019s \u201cderiving,\u201d we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 el 25 de agosto en el <a href=\"http:\/\/www.inf.kcl.ac.uk\/staff\/urbanc\/itp-2015\">ITP 2015<\/a> (<em>The 6th 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:\/\/cl-informatik.uibk.ac.at\/software\/ceta\/experiments\/deriving\">aqu\u00ed<\/a>.<\/p>\n<p>Este art\u00edculo puede servir de lectura complementaria en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a>, <a href=\"http:\/\/www.cs.us.es\/cursos\/rac\/\">Razonamiento asistido por ordenador<\/a> y <a href=\"http:\/\/www.cs.us.es\/~mjoseh\/LCyTM-15\">L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en Isabelle\/HOL titulado Deriving comparators and show functions in Isabelle\/HOL. Sus autores son Christian Sternagel y Ren\u00e9 Thiemann (del Computational Logic Research Group en la Universidad de Innsbruck, Austria). Su resumen es We present an Isabelle\/HOL development that allows for the automatic generation of certain operations&#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\/5023"}],"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=5023"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5023\/revisions"}],"predecessor-version":[{"id":5024,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5023\/revisions\/5024"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5023"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5023"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5023"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}