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.
The research leading to these results has received funding from the European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Avigad, J.: Methodology and metaphysics in the development of Dedekind’s theory of ideals. In: The Architecture of Modern Mathematics. Essays in History and Philosophy. Oxford University Press, Oxford (2006)
Barakat, M., Lange-Hegermann, M.: An axiomatic setup for algorithmic homological algebra and an alternative approach to localization. J. Algebra Appl. 10(2), 269–293 (2011)
Barakat, M., Robertz, D.: homalg – A Meta-Package for Homological Algebra. J. Algebra Appl. 7(3), 299–317 (2008)
Bourbaki, N.: Commutative algebra. Elements of Mathematics, ch. 1-7. Springer (1998)
COQ development team. The COQ Proof Assistant Reference Manual, version 8.3. Technical report (2010)
Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms: An introduction to Computational Algebraic Geometry and Commutative Algebra. Springer (2006)
Dénès, M., Mörtberg, A., Siles, V.: A Refinement-Based Approach to Computational Algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 83–98. Springer, Heidelberg (2012)
Ducos, L., Lombardi, H., Quitté, C., Salou, M.: Théorie algorithmique des anneaux arithmétiques, des anneaux de Prüfer et des anneaux de Dedekind. Journal of Algebra 281(2), 604–650 (2004)
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009)
Gonthier, G.: Point-Free, Set-Free Concrete Linear Algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 103–118. Springer, Heidelberg (2011)
Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Technical report, Microsoft Research INRIA (2009)
Lombardi, H., Perdry, H.: The Buchberger Algorithm as a Tool for Ideal Theory of Polynomial Rings in Constructive Mathematics (1998)
Lombardi, H., Quitté, C.: Algébre commutative, Méthodes constructives: Modules projectifs de type fini. Calvage et Mounet (2011)
Mines, R., Richman, F., Ruitenburg, W.: A Course in Constructive Algebra. Springer (1988)
Mörtberg, A.: Constructive Algebra in Functional Programming and Type Theory. Master’s thesis, Chalmers University of Technology (2010)
Perdry, H., Schuster, P.: Noetherian orders. Mathematical. Structures in Comp. Sci. 21(1), 111–124
Persson, H.: An Integrated Development of Buchberger’s Algorithm in Coq (2001)
Quadrat, A.: The fractional representation approach to synthesis problems: An algebraic analysis viewpoint part ii: Internal stabilization. SIAM J. Control Optim. 42(1), 300–320 (2003)
Théry, L.: A Certified Version of Buchberger’s Algorithm. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 349–364. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T., Mörtberg, A., Siles, V. (2012). Coherent and Strongly Discrete Rings in Type Theory. In: Hawblitzel, C., Miller, D. (eds) Certified Programs and Proofs. CPP 2012. Lecture Notes in Computer Science, vol 7679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35308-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-35308-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35307-9
Online ISBN: 978-3-642-35308-6
eBook Packages: Computer ScienceComputer Science (R0)