{"id":4378,"date":"2014-07-16T06:00:27","date_gmt":"2014-07-16T04:00:27","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4378"},"modified":"2014-07-15T18:52:50","modified_gmt":"2014-07-15T16:52:50","slug":"resena-a-coq-formalization-of-finitely-presented-modules","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-coq-formalization-of-finitely-presented-modules\/","title":{"rendered":"Rese\u00f1a: A Coq formalization of finitely presented modules"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre \u00e1lgebra titulado <a href=\"http:\/\/perso.crans.org\/cohen\/papers\/fpmods.pdf\">A Coq formalization of finitely presented modules<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/perso.crans.org\/cohen\">Cyril Cohen<\/a> y <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\">Anders M\u00f6rtberg<\/a> (de la <em>University of Gothenburg<\/em>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>This paper presents a formalization of constructive module theory in the intuitionistic type theory of Coq. We build an abstraction layer on top of matrix encodings, in order to represent finitely presented modules, and obtain clean definitions with short proofs justifying that it forms an abelian category. The goal is to use it as a first step to compute certified topological invariants, like homology groups and Betti numbers.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 hoy en el <a href=\"http:\/\/www.cs.uwyo.edu\/~ruben\/itp-2014\">ITP 2014<\/a> (<em>5th Conference on Interactive Theorem Proving<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/perso.crans.org\/cohen\/work\/fpmods\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre \u00e1lgebra titulado A Coq formalization of finitely presented modules. Sus autores son Cyril Cohen y Anders M\u00f6rtberg (de la University of Gothenburg). Su resumen es This paper presents a formalization of constructive module theory in the intuitionistic type theory of Coq. We build an&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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,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\/4378"}],"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=4378"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4378\/revisions"}],"predecessor-version":[{"id":4379,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4378\/revisions\/4379"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4378"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4378"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4378"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}