{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:58:48Z","timestamp":1767927528233,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642353079","type":"print"},{"value":"9783642353086","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_21","type":"book-chapter","created":{"date-parts":[[2012,11,7]],"date-time":"2012-11-07T22:20:18Z","timestamp":1352326818000},"page":"273-288","source":"Crossref","is-referenced-by-count":4,"title":["Coherent and Strongly Discrete Rings in Type Theory"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","volume-title":"The Architecture of Modern Mathematics. Essays in History and Philosophy","author":"J. Avigad","year":"2006","unstructured":"Avigad, J.: Methodology and metaphysics in the development of Dedekind\u2019s theory of ideals. In: The Architecture of Modern Mathematics. Essays in History and Philosophy. Oxford University Press, Oxford (2006)"},{"issue":"2","key":"21_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1142\/S0219498811004562","volume":"10","author":"M. Barakat","year":"2011","unstructured":"Barakat, M., Lange-Hegermann, M.: An axiomatic setup for algorithmic homological algebra and an alternative approach to localization. J. Algebra Appl.\u00a010(2), 269\u2013293 (2011)","journal-title":"J. Algebra Appl."},{"issue":"3","key":"21_CR3","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1142\/S0219498808002813","volume":"7","author":"M. Barakat","year":"2008","unstructured":"Barakat, M., Robertz, D.: homalg \u2013 A Meta-Package for Homological Algebra. J. Algebra Appl.\u00a07(3), 299\u2013317 (2008)","journal-title":"J. Algebra Appl."},{"key":"21_CR4","unstructured":"Bourbaki, N.: Commutative algebra. Elements of Mathematics, ch. 1-7. Springer (1998)"},{"key":"21_CR5","unstructured":"COQ development team. The COQ Proof Assistant Reference Manual, version 8.3. Technical report (2010)"},{"key":"21_CR6","unstructured":"Cox, D., Little, J., O\u2019Shea, D.: Ideals, Varieties and Algorithms: An introduction to Computational Algebraic Geometry and Commutative Algebra. Springer (2006)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-32347-8_7","volume-title":"Interactive Theorem Proving","author":"M. D\u00e9n\u00e8s","year":"2012","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A Refinement-Based Approach to Computational Algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 83\u201398. Springer, Heidelberg (2012)"},{"issue":"2","key":"21_CR8","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1016\/j.jalgebra.2004.06.030","volume":"281","author":"L. Ducos","year":"2004","unstructured":"Ducos, L., Lombardi, H., Quitt\u00e9, C., Salou, M.: Th\u00e9orie algorithmique des anneaux arithm\u00e9tiques, des anneaux de Pr\u00fcfer et des anneaux de Dedekind. Journal of Algebra\u00a0281(2), 604\u2013650 (2004)","journal-title":"Journal of Algebra"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"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.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-22863-6_10","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-Free, Set-Free Concrete Linear Algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 103\u2013118. Springer, Heidelberg (2011)"},{"key":"21_CR11","unstructured":"Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the Coq system. Technical report, Microsoft Research INRIA (2009)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Lombardi, H., Perdry, H.: The Buchberger Algorithm as a Tool for Ideal Theory of Polynomial Rings in Constructive Mathematics (1998)","DOI":"10.1017\/CBO9780511565847.023"},{"key":"21_CR13","unstructured":"Lombardi, H., Quitt\u00e9, C.: Alg\u00e9bre commutative, M\u00e9thodes constructives: Modules projectifs de type fini. Calvage et Mounet (2011)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Mines, R., Richman, F., Ruitenburg, W.: A Course in Constructive Algebra. Springer (1988)","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"21_CR15","unstructured":"M\u00f6rtberg, A.: Constructive Algebra in Functional Programming and Type Theory. Master\u2019s thesis, Chalmers University of Technology (2010)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Perdry, H., Schuster, P.: Noetherian orders. Mathematical. Structures in Comp. Sci.\u00a021(1), 111\u2013124","DOI":"10.1017\/S0960129510000460"},{"key":"21_CR17","unstructured":"Persson, H.: An Integrated Development of Buchberger\u2019s Algorithm in Coq (2001)"},{"issue":"1","key":"21_CR18","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1137\/S0363012902417139","volume":"42","author":"A. Quadrat","year":"2003","unstructured":"Quadrat, A.: The fractional representation approach to synthesis problems: An algebraic analysis viewpoint part ii: Internal stabilization. SIAM J. Control Optim.\u00a042(1), 300\u2013320 (2003)","journal-title":"SIAM J. Control Optim."},{"key":"21_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BFb0054271","volume-title":"Automated Deduction - CADE-15","author":"L. Th\u00e9ry","year":"1998","unstructured":"Th\u00e9ry, L.: A Certified Version of Buchberger\u2019s Algorithm. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 349\u2013364. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T09:13:48Z","timestamp":1620119628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}