Reseña: Coherent and strongly discrete rings in type theory
Se ha publicado un nuevo trabajo de formalización de las matemáticas en Coq titulado Coherent and strongly discrete rings in type theory.
Sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).
El trabajo se presentará en el CPP 2012 (The Second International Conference on Certified Programs and Proofs) que comenzará el 13 de diciembre.
Su resumen es
We 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ézout domains (for instance
and
) and Prüfer 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.
El código Coq de la formalización se encuentra aquí.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.