{"id":2147,"date":"2012-08-24T05:24:23","date_gmt":"2012-08-24T05:24:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2147"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"coherent-and-strongly-discrete-rings-in-type-theory","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/coherent-and-strongly-discrete-rings-in-type-theory\/","title":{"rendered":"Rese\u00f1a: Coherent and strongly discrete rings in type theory"},"content":{"rendered":"<p>Se ha publicado un nuevo trabajo de formalizaci\u00f3n de las matem\u00e1ticas en <a href=\"http:\/\/coq.inria.fr\">Coq<\/a> titulado <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\/papers\/coherent.pdf\">Coherent and strongly discrete rings in type theory<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.cse.chalmers.se\/~coquand\">Tierry Coquand<\/a>, <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\">Anders M\u00f6rtberg<\/a> y <a href=\"http:\/\/www.cse.chalmers.se\/~siles\">Vincent Siles<\/a> (de la Univ. de Gotemburgo, Suecia).<\/p>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/cpp12.kuis.kyoto-u.ac.jp\">CPP 2012<\/a> (<i>The Second International Conference on Certified Programs and Proofs<\/i>) que comenzar\u00e1 el 13 de diciembre.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present a formalization of coherent and strongly discrete rings in type theory. This is a fundamental structure in constructive algebra that represents rings in which it is possible to solve linear systems of equations. These structures have been instantiated with B\u00e9zout domains (for instance <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=%5Cmathbb%7BZ%7D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"&#92;mathbb{Z}\" class=\"latex\" \/> and <img decoding=\"async\" src=\"https:\/\/s0.wp.com\/latex.php?latex=k%5Bx%5D&#038;bg=ffffff&#038;fg=000&#038;s=0&#038;c=20201002\" alt=\"k[x]\" class=\"latex\" \/>) and Pr\u00fcfer domains (generalization of Dedekind domains) so that we get certified algorithms solving systems of equations that are applicable on these general structures. This work can be seen as basis for developing a formalized library of linear algebra over rings.\n<\/p><\/blockquote>\n<p>El c\u00f3digo Coq de la formalizaci\u00f3n se encuentra <a href=\"http:\/\/www.cse.chalmers.se\/~mortberg\/coherent\">aqu\u00ed<\/a>.<\/p>\n<p>Este trabajo es parte del proyecto <a href=\"http:\/\/wiki.portal.chalmers.se\/cse\/pmwiki.php\/ForMath\/ForMath\">ForMath: Formalisation of Mathematics<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un nuevo trabajo de formalizaci\u00f3n de las matem\u00e1ticas en Coq titulado Coherent and strongly discrete rings in type theory. Sus autores son Tierry Coquand, Anders M\u00f6rtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia). El trabajo se presentar\u00e1 en el CPP 2012 (The Second International Conference on Certified Programs and Proofs)&#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,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\/2147"}],"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=2147"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2147\/revisions"}],"predecessor-version":[{"id":2788,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2147\/revisions\/2788"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2147"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2147"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2147"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}