{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:23Z","timestamp":1767927803674,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665373","type":"print"},{"value":"9783540481676","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48167-2_3","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T07:40:19Z","timestamp":1191570019000},"page":"33-46","source":"Crossref","is-referenced-by-count":11,"title":["Gr\u00f6bner Bases in Type Theory"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Henrik","family":"Persson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"P. Aczel. An Introduction to Inductive Definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739\u2013782. North-Holland Publishing Company, 1977. 34, 37, 38","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"L. Augustsson. Cayenne-a language with dependent types. Technical report, Department of Computing Science, Chalmers University of Technology, 1998. Homepage: http:\/\/www.cs.chalmers.se\/~augustss\/cayenne\/ . 42","DOI":"10.1145\/289423.289451"},{"key":"3_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the Workshop TYPES\u2019 95, Torino, Italy, June 1995","author":"U. Berger","year":"1996","unstructured":"U. Berger and H. Schwichtenberg. The greatest common divisor: a case study for program extraction from classical proofs. In Proceedings of the Workshop TYPES\u2019 95, Torino, Italy, June 1995, number 1158 in Lecture Notes in Computer Science. Springer-Verlag, 1996. 34"},{"key":"3_CR4","unstructured":"B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal (German). PhD thesis, University of Innsbruck, 1965. 33"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"B. Buchberger. Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory. In N. K. Bose, editor, Multidimensional systems theory, pages 184\u2013232. Reidel Publ. Co., 1985. 33, 34","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"B. Buchberger. Introduction to Gr\u00f6bner bases. In B. Buchberger and F. Winkler, editors, Gr\u00f6bner bases and applications, pages 3\u201331. Cambridge University Press, 1998. 34","DOI":"10.1017\/CBO9780511565847.003"},{"key":"3_CR7","volume-title":"Graduate Texts in Mathematics","author":"T. Becker","year":"1993","unstructured":"T. Becker and V. Weispfenning. Gr\u00f6bner bases, volume 141 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1993. In cooperation with H. Kredel. 34, 35, 39, 42"},{"key":"3_CR8","volume-title":"Undergraduate Texts in Mathematics","author":"D. Cox","year":"1997","unstructured":"D. Cox, J. Little, and D. O\u2019Shea. Ideals, varieties, and algorithms. Undergraduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1997. 34","edition":"second edition"},{"key":"3_CR9","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986. 35"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","first-page":"28","volume-title":"proceeding of the conference Constructivity in Computer Science, San Antonio","author":"Th. Coquand","year":"1992","unstructured":"Th. Coquand. Constructive topology and combinatorics. In proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613, pages 28\u201332, 1992. 33, 34, 37, 38, 39"},{"key":"3_CR11","unstructured":"C. Coquand. The homepage of the Agda type checker. Homepage: http:\/\/www.cs.chalmers.se\/~catarina\/Agda\/ , 1998. 42"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L. E. Dickson","year":"1913","unstructured":"L. E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math., 35:413\u2013422, 1913. 34","journal-title":"Am. J. Math."},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/0167-6423(90)90058-L","volume":"14","author":"P. Dybjer","year":"1990","unstructured":"P. Dybjer. Comparing integrated and external logics of functional programs. Science of Computer Programming, 14:59\u201379, 1990. 33","journal-title":"Science of Computer Programming"},{"key":"3_CR14","unstructured":"R. Fr\u00f6berg. An introduction to Gr\u00f6bner bases. John Wiley & Sons, 1997. 34"},{"key":"3_CR15","series-title":"Lect Notes Comput Sci","first-page":"166","volume-title":"Mathematical Models for the Semantics of Parallelism","author":"J.-Y. Girard","year":"1986","unstructured":"J-Y Girard. Linear logic and parallelism. In M. Venturini Zilli, editor, Mathematical Models for the Semantics of Parallelism, number LNCS 280, pages 166\u2013182. Springer-Verlag, September 1986. 33"},{"key":"3_CR16","unstructured":"G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq proof assistant: A tutorial. Technical report, Rapport Technique 204, INRIA, 1997. 34"},{"key":"3_CR17","unstructured":"P. B. Jackson. Enhancing the Nuprl proof development system and applying it to computational abstract algebra. PhD thesis, Cornell University, 1995. 35, 41"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/S0747-7171(08)80154-X","volume":"12","author":"C. Jacobsson","year":"1991","unstructured":"C. Jacobsson and C. L\u00f6fwall. Standard bases for general coefficient rings and a new constructive proof of Hilbert\u2019s basis theorem. J. Symbolic Comput., 12(3):337\u2013371, 1991. 34, 39","journal-title":"J. Symbolic Comput."},{"key":"3_CR19","unstructured":"P. Martin-L\u00f6f. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968. 37"},{"key":"3_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8640-5","volume-title":"A course in constructive algebra","author":"R. Mines","year":"1988","unstructured":"R. Mines, F. Richman, and W. Ruitenburg. A course in constructive algebra. Universitext. Springer-Verlag, New York, 1988. 39"},{"key":"3_CR21","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f\u2019 s Type Theory. An Introduction. Oxford University Press, 1990. 33"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. Nash-Williams","year":"1963","unstructured":"C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833\u2013835, 1963. 41","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"3_CR23","unstructured":"L\u00d6c Pottier. Dixon\u2019s lemma. URL: ftp:\/\/www.inria.fr\/safir\/pottier\/MON , 1996. 34"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0020-0190(88)90126-3","volume":"29","author":"J.-C. Raoult","year":"1988","unstructured":"J-C. Raoult. Proving open properties by induction. Information processing letters, 29:19\u201323, 1988. 33, 34, 37, 39","journal-title":"Information processing letters"},{"key":"3_CR25","doi-asserted-by":"publisher","first-page":"436","DOI":"10.2307\/2040452","volume":"44","author":"F. Richman","year":"1974","unstructured":"F. Richman. Constructive aspects of noetherian rings. In Proc. AMS 44, pages 436\u2013441, 1974. 39","journal-title":"Proc. AMS"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"L. Th\u00e9ry. Proving and computing: A certified version of the Buchberger\u2019s algorithm. In proceeding of the 15th International Conference on Automated Deduction, Lindau, Germany, LNAI 1421, 1998. 34, 41","DOI":"10.1007\/BFb0054271"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48167-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T15:06:25Z","timestamp":1556895985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48167-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665373","9783540481676"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48167-2_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}