{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:29Z","timestamp":1725562589955},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_5","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"66-82","source":"Crossref","is-referenced-by-count":8,"title":["A Constructive Proof of Higman\u2019s Lemma in Isabelle"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Berghofer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"5_CR2","unstructured":"Barras, B., et al.: The Coq proof assistant reference manual \u2013 version 7.2. Technical Report 0255, INRIA (February 2002)"},{"key":"5_CR3","series-title":"Systems and Implementation Techniques of Applied Logic Series","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-94-017-0435-9_2","volume-title":"Automated Deduction \u2013 A Basis for Applications","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction \u2013 A Basis for Applications. Systems and Implementation Techniques of Applied Logic Series, vol.\u00a0II, pp. 41\u201371. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-39185-1_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2003","unstructured":"Berghofer, S.: Program Extraction in simply-typed Higher Order Logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 21\u201338. Springer, Heidelberg (2003)"},{"key":"5_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ (1986)"},{"key":"5_CR6","unstructured":"Coquand, T., Fridlender, D.: A proof of Higman\u2019s lemma by structural induction. Unpublished draft (November 1993), available at \n                  \n                    http:\/\/www.math.chalmers.se\/~frito\/Papers\/open.ps.gz"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/BFb0097789","volume-title":"Types for Proofs and Programs","author":"D. Fridlender","year":"1998","unstructured":"Fridlender, D.: Higman\u2019s lemma in type theory. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 112\u2013133. Springer, Heidelberg (1998)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society, vol.\u00a03(2), pp. 326\u2013336 (1952)","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"5_CR9","unstructured":"Magnusson, L.: The Implementation of ALF\u2014a Proof Editor Based on Martin- L\u00f6f \u2019s Monomorphic Type Theory with Explicit Substitution. Phd thesis, Dept. of Computing Science, Chalmers Univ. of Technology and Univ. of G\u00f6teborg (1994)"},{"key":"5_CR10","unstructured":"Murthy, C.: Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University (1990)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/LICS.1990.113752","volume-title":"Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science","author":"C.R. Murthy","year":"1990","unstructured":"Murthy, C.R., Russell, J.R.: A constructive proof of Higman\u2019s lemma. In: Mitchell, J.C. (ed.) Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA, June 1990, pp. 257\u2013269. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"4","key":"5_CR12","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. Nash-Williams","year":"1963","unstructured":"Nash-Williams, C.: On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society\u00a059(4), 833\u2013835 (1963)","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 49\u201392. Springer, Heidelberg (1993)"},{"key":"5_CR14","unstructured":"Seisenberger, M.: Konstruktive Aspekte von Higmans Lemma. Master\u2019s thesis, Fakult\u00e4t f\u00fcr Mathematik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (1998)"},{"key":"5_CR15","unstructured":"Seisenberger, M.: On the Constructive Content of Proofs. PhD thesis, Fakult\u00e4t f\u00fcr Mathematik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen (2003)"},{"key":"5_CR16","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Constructivism in Mathematics","author":"S. Troelstra","year":"1988","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"5_CR17","unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen (2002), \n                  \n                    http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:15:16Z","timestamp":1620011716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}