{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:38:05Z","timestamp":1759639085894},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540427520"},{"type":"electronic","value":"9783540455042"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45504-3_5","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T22:56:02Z","timestamp":1187045762000},"page":"68-77","source":"Crossref","is-referenced-by-count":0,"title":["Program Extraction from Gentzen\u2019s Proof of Transfinite Induction up to \u03b50"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,2]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.2307\/2272543","volume":"371","author":"P. Aczel","year":"1972","unstructured":"P. Aczel. Describing ordinals by functionals of transfinite type. Journal of Symbolic Logic 37(1), 35\u201347, 1972.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications (TLCA\u201993)","author":"U. Berger","year":"1993","unstructured":"U. Berger. Program extraction from normalization proofs. Typed Lambda Calculi and Applications (TLCA\u201993), LNCS 664, 91\u2013106, 1993."},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0168-0072(98)00046-3","volume":"97","author":"N. Danner","year":"1999","unstructured":"N. Danner. Ordinals and ordinal functions representable in the simply typed lambda calculus. Annals of Pure and Applied Logic 97, 179\u2013201, 1999.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"S. Feferman. Hereditarily replete functionals over the ordinals. Intuitionism and Proof theory, J. Myhill, editor, North-Holland, 289\u2013301, 1970.","DOI":"10.1016\/S0049-237X(08)70760-2"},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/BF01564760","volume":"119","author":"G. Gentzen","year":"1943","unstructured":"G. Gentzen. Beweisbarkeit undUn beweisbarkeit von Anfangsf\u00e4llen der transfiniten Induktion in der reinen Zahlentheorie. Mathematische Annalen 119, 140\u2013161, 1943.","journal-title":"Mathematische Annalen"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"K. G\u00f6del. \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes. Dialectica 12, 280\u2013287, 1958.","journal-title":"Dialectica"},{"key":"5_CR7","unstructured":"P. Hancock. Ordinals and Interactive Programs. Unpublished, 2001."},{"key":"5_CR8","unstructured":"G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, A. Heyting, editor, North-Holland, 101\u2013128, 1959."},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF01174155","volume":"58","author":"W. Neumer","year":"1953","unstructured":"W. Neumer. Zur Konstruktion von Ordnungszahlen. Mathematische Zeitschrift. I, vol. 58, 319\u2013413, 1953; II, vol. 59, 434-454, 1954; III, vol. 60, 1-16, 1954; IV, vol. 61, 47-69, 1954; V, vol. 64, 435-456, 1956.","journal-title":"Mathematische Zeitschrift"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1002\/malq.19570030604","volume":"3","author":"W. Neumer","year":"1957","unstructured":"W. Neumer. Algorithmen f\u00fcr Ordnungzahlen und Normalfunktionen. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik. I, vol. 3, 108\u2013150, 1957; II, vol. 6, 1-65, 1960.","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"W. Pohlers. Proof Theory. SLNM 1407, 1989.","DOI":"10.1007\/978-3-540-46825-7"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1002\/malq.19710170113","volume":"17","author":"H. Schwichtenberg","year":"1971","unstructured":"H. Schwichtenberg. Eine Klassifikation der e0-rekursiven Funktionen. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik 17, 61\u201374, 1971.","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"5_CR13","unstructured":"H. Schwichtenberg. Einige Anwendungen von unendlichen Termen und Wertfunktionalen. Mathematisches Institut der Universit\u00e4t M\u00fcnster, Habilitationsschrift, 1973."},{"key":"5_CR14","first-page":"279","volume":"73","author":"H. Schwichtenberg","year":"1975","unstructured":"H. Schwichtenberg. Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion. Logic Colloquium 73 North-Holland, 279\u2013303, 1975.","journal-title":"Logic Colloquium"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg. Classifying Recursive Functions. In: E. Griffor, editor, Handbook of Recursion Theory, 533\u2013586, North-Holland, 1999.","DOI":"10.1016\/S0049-237X(99)80032-9"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2273149","volume":"47","author":"J. Terlouw","year":"1982","unstructured":".J. Terlouw. On definition trees of ordinal recursive functionals: reduction of the recursion orders by means of type level raising. Journal of Symbolic Logic 47, 395\u2013402, 1982.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0168-0072(85)90031-4","volume":"28","author":"J. Terlouw","year":"1985","unstructured":"J. Terlouw. Reduction of higher type levels by means of an ordinal analysis of finite terms. Annals of Pure and Applied Logic 28, 73\u2013102, 1985.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra. Metamathematical Investigations of Intuitionistic Arithmetic and Analysis. SLNM 344, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"5_CR19","unstructured":"A. S. Troelstra and Dirk van Dalen. Constructivism in Mathematics. An Introduction. Volumes 121 and 123 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1988."}],"container-title":["Lecture Notes in Computer Science","Proof Theory in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45504-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T00:53:14Z","timestamp":1556758394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45504-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427520","9783540455042"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45504-3_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}