{"id":3145,"date":"2013-03-30T06:22:52","date_gmt":"2013-03-30T06:22:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3145"},"modified":"2013-03-30T06:30:14","modified_gmt":"2013-03-30T06:30:14","slug":"resena-programming-and-reasonning-with-powerlists-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-programming-and-reasonning-with-powerlists-in-coq\/","title":{"rendered":"Rese\u00f1a: Programming and reasonning with PowerLists in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> sobre programas paralelos titulado <a href=\"http:\/\/www.univ-orleans.fr\/lifo\/prodsci\/rapports\/RR\/RR2013\/RR-2013-02.pdf\">Programming and reasonning with PowerLists in Coq<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li> <a href=\"http:\/\/frederic.loulergue.eu\/index.html\">Fr\u00e9d\u00e9ric Loulergue<\/a> (de la Univ. de Orleans, Francia) y\n<li> <a href=\"http:\/\/www.cs.ubbcluj.ro\/~vniculescu\">Virginia Niculescu<\/a> (de la Univ. Babes-Bolyai de Cluj-Napoca, Ruman\u00eda).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nFor parallel programs correctness by construction is an essential feature since debugging is almost impossible. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. <a href=\"http:\/\/www.cs.utexas.edu\/users\/psp\/powerlist.pdf\">PowerLists<\/a> theory and the variants represent a good theoretical base for an approach like this, and Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the PowerList theory in Coq, and to use this modelling to program and reason on parallel programs in Coq. This represents the first step in building a framework that ease the development of correct and verifiable parallel programs.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las teor\u00edas desarrolladas en Coq se encuentra <a href=\"http:\/\/traclifo.univ-orleans.fr\/SDPP\/wiki\/PowerLists\">aqu\u00ed<\/a>.    <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre programas paralelos titulado Programming and reasonning with PowerLists in Coq. Sus autores son Fr\u00e9d\u00e9ric Loulergue (de la Univ. de Orleans, Francia) y Virginia Niculescu (de la Univ. Babes-Bolyai de Cluj-Napoca, Ruman\u00eda). Su resumen es For parallel programs correctness by construction is an essential feature&#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":[100],"tags":[45,273,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\/3145"}],"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=3145"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3145\/revisions"}],"predecessor-version":[{"id":3149,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3145\/revisions\/3149"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3145"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3145"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3145"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}