{"id":3509,"date":"2013-08-14T06:46:09","date_gmt":"2013-08-14T06:46:09","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3509"},"modified":"2013-08-14T06:46:09","modified_gmt":"2013-08-14T06:46:09","slug":"generic-datatypes-a-la-carte","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/generic-datatypes-a-la-carte\/","title":{"rendered":"Generic datatypes \u00e0 la carte"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> titulado <a href=\"http:\/\/users.ugent.be\/~skeuchel\/publications\/gdtc.pdf\">Generic datatypes \u00e0 la carte<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/users.ugent.be\/~skeuchel\/\">Steven Keuchel<\/a> y <a href=\"http:\/\/users.ugent.be\/~tschrijv\/index.html\">Tom Schrijvers<\/a> (de la Universidad de Gante, B\u00e9lgica).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nFormal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory \u00e0 la Carte (MTC) framework in the context of programming language meta-theory. However, MTC\u2019s use of extensible Church-encodings is unsatisfactory. <\/p>\n<p>This paper takes a better approach to the problem with datatype- generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.\n<\/p><\/blockquote>\n<p>El correspondiente c\u00f3digo en Coq se encuentra <a href=\"https:\/\/github.ugent.be\/skeuchel\/gdtc\">aqu\u00ed<\/a>.<\/p>\n<p>El trabajo se presentar\u00e1 en el  <a href=\"http:\/\/www.wgp-sigplan.org\/2013\/\">WGP 2013<\/a> (<i>9th ACM SIGPLAN Workshop on Generic Programming<\/i>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento en Coq titulado Generic datatypes \u00e0 la carte. Sus autores son Steven Keuchel y Tom Schrijvers (de la Universidad de Gante, B\u00e9lgica). Su resumen es Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue&#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":[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\/3509"}],"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=3509"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3509\/revisions"}],"predecessor-version":[{"id":3510,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3509\/revisions\/3510"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3509"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3509"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3509"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}