{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:48Z","timestamp":1767928008107,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540651376","type":"print"},{"value":"9783540495628","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097789","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"112-133","source":"Crossref","is-referenced-by-count":7,"title":["Higman's lemma in type theory"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Fridlender","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"P. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In 11th Annual IEEE Symposium on Logic in Computer Science. Proceedings, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In 8th Annual IEEE Symposium on Logic in Computer Science. Proceedings, pages 160\u2013170, 1993.","DOI":"10.1109\/LICS.1993.287591"},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4153\/CJM-1954-001-9","volume":"6","author":"L. Brouwer","year":"1954","unstructured":"L. Brouwer. Points and spaces. Canadian Journal of Mathematics, 6:1\u201317, 1954.","journal-title":"Canadian Journal of Mathematics"},{"key":"7_CR4","unstructured":"H. Curry and R. Feys. Combinatory Logic, volume I. North-Holland, 1958."},{"key":"7_CR5","unstructured":"T. Coquand, D. Fridlender, and H. Herbelin. A proof of higman's lemma by structural induction. Unpublished manuscript, 1993."},{"key":"7_CR6","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"R. Constable","year":"1986","unstructured":"R. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"7_CR7","unstructured":"T. Coquand. Pattern matching with dependent types. In Proceeding from the logical framework workshop at B\u00e5stad, June 1992."},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"L. Dickson","year":"1913","unstructured":"L. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35:413\u2013426, 1913.","journal-title":"American Journal of Mathematics"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, page 273. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"7_CR10","volume-title":"Elements of intuitionism","author":"M. Dummett","year":"1977","unstructured":"M. Dummett. Elements of intuitionism. Clarendon Press, Oxford, 1977."},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440\u2013465, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"255","DOI":"10.2307\/2306526","volume":"59","author":"P. Erd\u00f6s","year":"1952","unstructured":"P. Erd\u00f6s and R. Rado. Sets having a divisor property. American Mathematical Monthly, 59:255\u2013257, 1952.","journal-title":"American Mathematical Monthly"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"480","DOI":"10.2307\/2305141","volume":"56","author":"P. Erd\u00f6s","year":"1949","unstructured":"P. Erd\u00f6s. Problem 4358. American Mathematical Monthly, 56:480, 1949.","journal-title":"American Mathematical Monthly"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"H. Friedman. Classically and intuitionistically provably recursive functions. In D. Scott and G. Muller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21\u201328. Springer-Verlag, 1978.","DOI":"10.1007\/BFb0103100"},{"key":"7_CR15","unstructured":"D. Fridlender. Ramsey's theorem in type theory. Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, October 1993."},{"key":"7_CR16","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"K. G\u00f6del. Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse eines mathematischen Kolloquiums, 4:34\u201338, 1933. English: [G\u00f6d65].","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"7_CR17","unstructured":"K. G\u00f6del. On intuitionistic arithmetic and number theory. In M. Davis, editor, The Undecidable, pages 75\u201381, Raven Press, 1965."},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1016\/S0021-9800(69)80111-0","volume":"6","author":"L. Haines","year":"1969","unstructured":"L. Haines. On free monoids partially ordered by embedding. Journal of Combinatorial Theory, 6:94\u201398, 1969.","journal-title":"Journal of Combinatorial Theory"},{"issue":"3","key":"7_CR19","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, (3) 2:326\u2013336, 1952.","journal-title":"Proceedings of the London Mathematical Society"},{"key":"7_CR20","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W. Howard","year":"1980","unstructured":"W. Howard. The formulae-as-types notion of construction. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, London, 1980."},{"key":"7_CR21","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/1385-7258(77)90067-1","volume":"39","author":"D. Jongh de","year":"1977","unstructured":"D. de Jongh and R. Parikh. Well-partial orderings and hierarchies. Indagationes Mathematicae, 39:195\u2013207, 1977.","journal-title":"Indagationes Mathematicae"},{"key":"7_CR22","first-page":"851","volume":"266","author":"P. Jullien","year":"1968","unstructured":"P. Jullien. Sur un th\u00e9or\u00e8me d'extension dans la th\u00e9orie des mots. Comptes Rendus de la Academie de Sciences de Paris, (A) 266:851\u2013854, 1968.","journal-title":"Comptes Rendus de la Academie de Sciences de Paris"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"210","DOI":"10.2307\/1993287","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"J. Kruskal. Well-Quasi-Ordering, the tree theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210\u2013225, 1960.","journal-title":"Transactions of the American Mathematical Society"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0097-3165(72)90063-5","volume":"13","author":"J. Kruskal","year":"1972","unstructured":"J. Kruskal. The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept. Journal of Combinatorial Theory (A), 13:297\u2013305, 1972.","journal-title":"Journal of Combinatorial Theory (A)"},{"key":"7_CR25","unstructured":"L. Magnusson. The Implementation of ALF\u2014a Proof Editor based on Martin-L\u00f6f's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Department of Computing Science, Chalmers University of Technology and University of G\u00f6teborg, 1994."},{"key":"7_CR26","unstructured":"P. Martin-L\u00f6f. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968."},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973, pages 73\u2013118, Amsterdam, 1975. North-Holland Publishing Company.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"7_CR28","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984."},{"key":"7_CR29","unstructured":"E. Martino and P. Giaretta. Brouwer, dummett and the bar theorem. In Atti del Convengo Nazionale di Logica. Bibliopolis, 1979."},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"C. Murthy and J. Russell. A constructive proof of higman's lemma. In Fifth annual IEEE Symposium on Logic in Computer Science, pages 257\u2013267, 1990.","DOI":"10.1109\/LICS.1990.113752"},{"key":"7_CR31","unstructured":"C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, 1990."},{"key":"7_CR32","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.","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"7_CR33","doi-asserted-by":"publisher","first-page":"202","DOI":"10.2307\/1990552","volume":"66","author":"B. Neumann","year":"1949","unstructured":"B. Neumann. On ordered division rings. Transaction of the American Mathematical Society, 66:202\u2013252, 1949.","journal-title":"Transaction of the American Mathematical Society"},{"key":"7_CR34","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1006\/aima.1993.1004","volume":"97","author":"F. Richman","year":"1993","unstructured":"F. Richman and G. Stolzenberg. Well Quasi-Ordered Sets. Advances in Mathematics, 97:145\u2013153, 1993.","journal-title":"Advances in Mathematics"},{"key":"7_CR36","unstructured":"D. Schmidt. Well-Partial-Orderings and Their Maximal Order Types. Habilitationsschrift, 1979."},{"key":"7_CR37","doi-asserted-by":"publisher","first-page":"961","DOI":"10.2307\/2274585","volume":"53","author":"S. Simpson","year":"1988","unstructured":"S. Simpson. Ordinal numbers and the hilbert basis theorem. The Journal of Symbolic Logic, 53:961\u2013974, 1988.","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"840","DOI":"10.2307\/2274575","volume":"53","author":"J. Smith","year":"1988","unstructured":"J. Smith. The Independence of Peano's Fourth Axiom from Martin-L\u00f6f's Type Theory without Universes. Journal of Symbolic Logic, 53:840\u2013845, 1988.","journal-title":"Journal of Symbolic Logic"},{"key":"7_CR39","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF02007558","volume":"25","author":"K. Sch\u00fctte","year":"1985","unstructured":"K. Sch\u00fctte and S. Simpson. Ein in der reinen zahlentheorie unberweisbarer satz \u00fcber endliche folgen von nat\u00fcrlichen zahlen. Archiv f\u00fcr Mathematische Logik und Grundlagenfroschung, 25:75\u201389, 1985.","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenfroschung"},{"key":"7_CR40","unstructured":"A. Tasistro. Substitution, record types and subtyping in type theory, with applications to the theory of programming. PhD thesis, Department of Computing Science at Chalmers University of Technology and University of G\u00f6teborg, 1997."},{"issue":"2","key":"7_CR41","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1112\/jlms\/s2-47.2.193","volume":"47","author":"W. Veldman","year":"1993","unstructured":"W. Veldman and M. Bezem. Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, (2) 47:193\u2013211, 1993.","journal-title":"Journal of the London Mathematical Society"},{"key":"7_CR42","unstructured":"W. Veldman. Intuitionistic proof of the general non-decidable case of higman's lemma. Personal communication, 1994."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097789","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T04:25:25Z","timestamp":1736655925000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097789"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/bfb0097789","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}