{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T06:15:12Z","timestamp":1775628912742,"version":"3.50.1"},"reference-count":5,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[1991,9,1]],"date-time":"1991-09-01T00:00:00Z","timestamp":683683200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch Math Logic"],"published-print":{"date-parts":[[1991,9]]},"DOI":"10.1007\/bf01621476","type":"journal-article","created":{"date-parts":[[2005,4,30]],"date-time":"2005-04-30T13:21:14Z","timestamp":1114867274000},"page":"405-408","source":"Crossref","is-referenced-by-count":21,"title":["An upper bound for reduction sequences in the typed \u03bb-calculus"],"prefix":"10.1007","volume":"30","author":[{"given":"Helmut","family":"Schwichtenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"109","volume-title":"Contributions to mathematical logic","author":"J. Diller","year":"1968","unstructured":"Diller, J.: Zur Berechenbarkeit primitiv-rekursiver Funktionale endlicher Typen. In: Sch\u00fctte, K. (ed.) Contributions to mathematical logic. Amsterdam: North-Holland 1968, pp. 109\u2013120"},{"key":"CR2","unstructured":"Gandy, R.O.: Proofs of strong normalization. In: Seldin, J.O., Hindley, J.R. (eds.) To H.B. Curry: Essays on combinatory logic, lambda calculus, and formalism. Academic Press 1980, pp. 457\u2013477"},{"issue":"3","key":"CR3","doi-asserted-by":"crossref","first-page":"493","DOI":"10.2307\/2273417","volume":"45","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: Ordinal analysis of terms of finite type. J. Symb. Logic,45 (3), 493\u2013504 (1980)","journal-title":"J. Symb. Logic"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1305\/ndjfl\/1093956080","volume":"8","author":"L.E. Sanchis","year":"1967","unstructured":"Sanchis, L.E.: Functional defined by recursion. Notre Dame J. Formal Logic8, 161\u2013174 (1967)","journal-title":"Notre Dame J. Formal Logic"},{"key":"CR5","first-page":"453","volume-title":"The L.E.J. Brouwer Centenary Symposium","author":"H. Schwichtenberg","year":"1982","unstructured":"Schwichtenberg, H.: Complexity of normalization in the pure typed\u03bb-calculus. In: Troelstra, A.S., Dalen, D. van (eds.): The L.E.J. Brouwer Centenary Symposium. Proceedings of the Conference held in Noordwijkerhout, 8\u201313 June, 1981. North-Holland, Studies in Logic and the Foundations of Mathematics. Amsterdam 1982, pp. 453\u2013458"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01621476.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01621476\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01621476","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T12:34:08Z","timestamp":1556886848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01621476"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,9]]},"references-count":5,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[1991,9]]}},"alternative-id":["BF01621476"],"URL":"https:\/\/doi.org\/10.1007\/bf01621476","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,9]]}}}