Coherent and strongly discrete rings in type theory

5Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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 k[x]) 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. © 2012 Springer-Verlag Berlin Heidelberg.

Cite

CITATION STYLE

APA

Coquand, T., Mörtberg, A., & Siles, V. (2012). Coherent and strongly discrete rings in type theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 273–288). https://doi.org/10.1007/978-3-642-35308-6_21

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free