{"id":2116,"date":"2012-08-08T16:57:19","date_gmt":"2012-08-08T16:57:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2116"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"resena-representation-coinductive-des-graphes","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-representation-coinductive-des-graphes\/","title":{"rendered":"Rese\u00f1a: Repr\u00e9sentation coinductive des graphes"},"content":{"rendered":"<p>Se ha publicado una nueva tesis de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a>: <a href=\"http:\/\/www.irit.fr\/~Celia.Picard\/These\/TheseCeliaPicard.pdf\">Repr\u00e9sentation coinductive des graphes<\/a>. <\/p>\n<p>Su autora es <a href=\"http:\/\/www.irit.fr\/~Celia.Picard\/\">Celia Picard<\/a> dirigida por <a href=\"http:\/\/www.irit.fr\/~Ralph.Matthes\">Ralph Matthes<\/a>.<\/p>\n<p>La tesis se present\u00f3 el 15 de junio en la Universidad de Toulouse (Universit\u00e9 Toulouse III Paul Sabatier).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n<b>Contexte g\u00e9n\u00e9ral<\/b><\/p>\n<p>Ce travail s\u2019inscrit \u00e0 l\u2019interface de l\u2019Ing\u00e9nierie Dirig\u00e9e par les Mod\u00e8les et de la th\u00e9orie des types. Dans le contexte toulousain, fortement ax\u00e9 vers les syst\u00e8mes embarqu\u00e9s et critiques, savoir certifier la repr\u00e9sentation et la transformation des mod\u00e8les est un enjeu majeur. La perspective vis\u00e9e ici est la transformation d\u2019un mod\u00e8le conforme \u00e0 un m\u00e9tamod\u00e8le en un mod\u00e8le conforme \u00e0 un autre m\u00e9tamod\u00e8le en assurant certaines propri\u00e9t\u00e9s sur le mod\u00e8le d\u2019arriv\u00e9e. Deux solutions sont possibles pour cela : v\u00e9rifier les propri\u00e9t\u00e9s sur chaque mod\u00e8le d\u2019arriv\u00e9e ou certifier que l\u2019application de la transformation assure ces propri\u00e9t\u00e9s. Nous avons choisi cette seconde solution. Pour la certification, nous avons d\u00e9cid\u00e9 dans un premier temps d\u2019utiliser un prouveur interactif, le syst\u00e8me Coq. La premi\u00e8re \u00e9tape consiste \u00e0 repr\u00e9senter les m\u00e9tamod\u00e8les, la seconde \u00e0 \u00e9tablir un langage permettant d\u2019exprimer les propri\u00e9t\u00e9s \u00e0 v\u00e9rifier. Dans cette th\u00e8se, nous nous int\u00e9ressons \u00e0 la repr\u00e9sentation et la manipulation de m\u00e9tamod\u00e8les sous forme de graphes. <\/p>\n<p><b>La repr\u00e9sentation des graphes<\/b><\/p>\n<p>Nous avons d\u00e9cid\u00e9 de repr\u00e9senter les graphes par des types coinductifs dont nous voulions explorer l\u2019utilisation dans Coq. En effet, la repr\u00e9sentation de la coindition dans les prouveurs bas\u00e9s sur la th\u00e9orie des types est en progr\u00e8s continuel. De plus, l\u2019utilisation des types coinductifs permet de rendre succincte et \u00e9l\u00e9gante notre repr\u00e9sentation des graphes et d\u2019obtenir la navigabilit\u00e9 par construction. Nous avons d\u00fb contourner la condition de garde dont le but est d\u2019assurer la validit\u00e9 des op\u00e9rations effectu\u00e9es sur les objets coinductifs. Son implantation dans Coq (compromis entre expressivit\u00e9 et maniabilit\u00e9, r\u00e9sultat d\u2019une longue \u00e9volution) est restrictive, et interdit parfois des d\u00e9finitions s\u00e9mantiquement correctes. Une formalisation canonique des graphes d\u00e9passe ainsi l\u2019expressivit\u00e9 directe de Coq. Nous avons donc propos\u00e9 une solution respectant ces limitations, puis nous nous sommes int\u00e9ress\u00e9s \u00e0 la d\u00e9finition d\u2019une relation plus permissive sur les graphes. Celle-ci permet d\u2019obtenir la m\u00eame notion d\u2019\u00e9quivalence qu\u2019avec une repr\u00e9sentation classique (ensemble de n\u0153uds\/ensemble d\u2019ar\u00eates) tout en gardant les avantages de la coinduction. En effet, notre d\u00e9finition des graphes cr\u00e9e un ordre implicite (horizontal et vertical) entre les n\u0153uds. Notre nouvelle relation permet de nous en affranchir. Nous montrons qu\u2019elle est \u00e9quivalente \u00e0 une relation bas\u00e9e sur des observations finies des graphes. Ces r\u00e9sultats ont fait l\u2019objet de publications et sont certifi\u00e9s par des d\u00e9veloppements Coq. Toutefois, ces derniers ont \u00e9t\u00e9 transcrits en langage math\u00e9matique et la lecture de cette th\u00e8se ne requiert pas de connaissance de Coq.\n<\/p><\/blockquote>\n<p>La formalizaci\u00f3n en Coq se encuentra <a href=\"http:\/\/www.irit.fr\/~Celia.Picard\/These\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado una nueva tesis de razonamiento formalizado en Coq: Repr\u00e9sentation coinductive des graphes. Su autora es Celia Picard dirigida por Ralph Matthes. La tesis se present\u00f3 el 15 de junio en la Universidad de Toulouse (Universit\u00e9 Toulouse III Paul Sabatier). Su resumen es Contexte g\u00e9n\u00e9ral Ce travail s\u2019inscrit \u00e0 l\u2019interface de l\u2019Ing\u00e9nierie Dirig\u00e9e&#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\/2116"}],"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=2116"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2116\/revisions"}],"predecessor-version":[{"id":2800,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2116\/revisions\/2800"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2116"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2116"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2116"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}