{"id":2125,"date":"2012-08-15T07:10:22","date_gmt":"2012-08-15T07:10:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2125"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"resena-formalization-of-shannon%e2%80%99s-theorems-in-ssreflect-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-shannon%e2%80%99s-theorems-in-ssreflect-coq\/","title":{"rendered":"Rese\u00f1a: Formalization of Shannon\u2019s theorems in SSReflect-Coq"},"content":{"rendered":"<p>Se ha publicado un nuevo art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a>, titulado <a href=\"http:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/affeldt-itp2012-preprint.pdf\">Formalization of Shannon\u2019s theorems in SSReflect-Coq<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/staff.aist.go.jp\/reynald.affeldt\">Reynald Affeldt<\/a> y <a href=\"http:\/\/staff.aist.go.jp\/hagiwara.hagiwara\">Manabu Hagiwara<\/a> (del <a href=\"http:\/\/www.aist.go.jp\">National Institute of Advanced Industrial Science and Technology<\/a> en Tsukuba, Jap\u00f3n). <\/p>\n<p>El trabajo se present\u00f3 ayer en el <a href=\"http:\/\/itp2012.cs.princeton.edu\">ITP 2012<\/a> (Interactive Theorem Proving).<\/p>\n<p>El resumen del trabajo es<\/p>\n<blockquote><p>\nThe most fundamental results of information theory are Shannon\u2019s theorems. These theorems express the bounds for reliable data compression and transmission over a noisy channel. Their proofs are non-trivial but rarely detailed, even in the introductory literature. This lack of formal foundations makes it all the more unfortunate that crucial results in computer security rely solely on information theory (the so-called \u201cunconditional security\u201d). In this paper, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem (that introduces the entropy as the bound for lossless compression), and the direct part of the more difficult channel coding theorem (that introduces the capacity as the bound for reliable communication over a noisy channel).\n<\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n se encuentra <a href=\"http:\/\/staff.aist.go.jp\/reynald.affeldt\/shannon\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un nuevo art\u00edculo de razonamiento formalizado en Coq, titulado Formalization of Shannon\u2019s theorems in SSReflect-Coq. Sus autores son Reynald Affeldt y Manabu Hagiwara (del National Institute of Advanced Industrial Science and Technology en Tsukuba, Jap\u00f3n). El trabajo se present\u00f3 ayer en el ITP 2012 (Interactive Theorem Proving). El resumen del trabajo es&#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,89,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\/2125"}],"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=2125"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2125\/revisions"}],"predecessor-version":[{"id":2796,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2125\/revisions\/2796"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2125"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2125"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2125"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}