{"id":3254,"date":"2013-04-25T06:02:25","date_gmt":"2013-04-25T06:02:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3254"},"modified":"2013-04-25T06:02:25","modified_gmt":"2013-04-25T06:02:25","slug":"resena-a-constructive-theory-of-regular-languages-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-constructive-theory-of-regular-languages-in-coq\/","title":{"rendered":"Rese\u00f1a: A constructive theory of regular languages in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> titulado <a href=\"http:\/\/www.ps.uni-saarland.de\/Publications\/documents\/DoczkalEtAl_2013_A-Constructive.pdf\">A constructive theory of regular languages in Coq<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.ps.uni-saarland.de\/~doczkal\/\">Christian Doczkal<\/a>, <a href=\"http:\/\/www.ps.uni-saarland.de\/~jokaiser\/\">Jan-Oliver Kaiser<\/a> y <a href=\"http:\/\/www.ps.uni-saarland.de\/~smolka\/\">Gert Smolka<\/a> (de la Univ. de Sarre (en alem\u00e1n: <i>Saarland<\/i>), Alemania). <\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present a formal constructive theory of regular languages consisting of about 1400 lines of Coq\/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect&#8217;s support for finite types and graphs.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/www.ps.uni-saarland.de\/~doczkal\/regular\/ConstructiveRegularLanguages.tgz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado A constructive theory of regular languages in Coq. Sus autores son Christian Doczkal, Jan-Oliver Kaiser y Gert Smolka (de la Univ. de Sarre (en alem\u00e1n: Saarland), Alemania). Su resumen es We present a formal constructive theory of regular languages consisting of about 1400 lines&#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\/3254"}],"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=3254"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3254\/revisions"}],"predecessor-version":[{"id":3255,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3254\/revisions\/3255"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3254"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3254"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3254"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}