{"id":2102,"date":"2012-07-26T05:40:15","date_gmt":"2012-07-26T05:40:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2102"},"modified":"2013-03-08T05:48:14","modified_gmt":"2013-03-08T05:48:14","slug":"resena-mechanization-of-an-algorithm-for-deciding-kat-terms-equivalence","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-mechanization-of-an-algorithm-for-deciding-kat-terms-equivalence\/","title":{"rendered":"Rese\u00f1a: Mechanization of an algorithm for deciding KAT terms equivalence"},"content":{"rendered":"<p>Se ha publicado un nuevo trabajo sobre verificaci\u00f3n formal en Coq: <a href=\"http:\/\/www.dcc.fc.up.pt\/dcc\/Pubs\/TReports\/TR12\/dcc-2012-04.pdf\">Mechanization of an algorithm for deciding KAT terms equivalence<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.dcc.fc.up.pt\/~nam\/web\">Nelma Moreira<\/a>, David Pereira y <a href=\"http:\/\/www.di.ubi.pt\/~desousa\">Simao Melo de Sousa<\/a> (de la <a href=\"http:\/\/www.up.pt\">Universidade do Porto<\/a>, Portugal).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence of <a href=\"http:\/\/web.mornfall.net\/stuff\/public_html\/.gio123\/p427-kozen.pdf\">Kleene algebra with tests<\/a> (KAT) terms. This mechanization was carried out in the <a href=\"http:\/\/coq.inria.fr\">Coq proof assistant<\/a>. The algorithm decides KAT terms equivalence through an iterated process of testing the equivalence of their partial derivatives. It is a purely syntactical decision procedure and so, it does not construct the underlying automata. The motivation for this work comes from the possibility of using KAT encoding of propositional Hoare logic for reasoning about the partial correctness of imperative programs.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n en Coq se encuentra <a href=\"http:\/\/www.liacc.up.pt\/~kat\/equivKAT.tgz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un nuevo trabajo sobre verificaci\u00f3n formal en Coq: Mechanization of an algorithm for deciding KAT terms equivalence. Sus autores son Nelma Moreira, David Pereira y Simao Melo de Sousa (de la Universidade do Porto, Portugal). Su resumen es This work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence&#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,89,285,275],"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\/2102"}],"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=2102"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2102\/revisions"}],"predecessor-version":[{"id":2804,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2102\/revisions\/2804"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2102"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2102"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2102"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}