{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:24Z","timestamp":1725664704047},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633853"},{"type":"electronic","value":"9783540698067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63385-5_54","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:26:41Z","timestamp":1330298801000},"page":"335-348","source":"Crossref","is-referenced-by-count":0,"title":["Upper bounds for standardizations and an application"],"prefix":"10.1007","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"27_CR1","unstructured":"H.P. Barendregt et al. (1976), Some notes on lambda reduction, Preprint No. 22, University of Utrecht, Department of mathematics, pp. 13\u201353."},{"key":"27_CR2","volume-title":"The Lambda Calculus: Its Syntax And Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"H.P. Barendregt (1984), The Lambda Calculus: Its Syntax And Semantics, North-Holland publishing company, Amsterdam."},{"key":"27_CR3","volume-title":"S\u00e9quentialit\u00e9 de l'\u00e9valuation formelle des \u03bb-expressions","author":"G. Berry","year":"1978","unstructured":"G. Berry (1978), S\u00e9quentialit\u00e9 de l'\u00e9valuation formelle des \u03bb-expressions, Proc. 3-e Colloque International sur la Programmation, Paris."},{"key":"27_CR4","volume-title":"The calculi of lambda conversion","author":"A. Church","year":"1941","unstructured":"A. Church, (1941), The calculi of lambda conversion, Princeton University Press, Princeton."},{"key":"27_CR5","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"H.B. Curry and R. Feys (1958), Combinatory Logic, North-Holland Publishing Company, Amsterdam."},{"key":"27_CR6","doi-asserted-by":"crossref","first-page":"339","DOI":"10.2307\/2274219","volume":"50","author":"R. Vrijer de","year":"1985","unstructured":"R. de Vrijer (1985), A direct proof of the finite developments theorem, Journal of Symbolic Logic, 50:339\u2013343.","journal-title":"Journal of Symbolic Logic"},{"key":"27_CR7","unstructured":"R.O. Gandy (1980), An early proof of normalization by A.M. Turing, To: H.B. Curry: Essays on combinatory logic, lambda calculus and formalism, edited by J.P. Seldin and J.R. Hindley, Academic press, pp. 453\u2013456."},{"key":"27_CR8","unstructured":"R.O. Gandy (1980), Proofs of Strong Normalization, To: H.B. Curry: Essays on Combinatory logic, lambda calculus and formalism, edited by J.P. Seldin and J.R. Hindley, Academic press, pp. 457\u2013478."},{"key":"27_CR9","unstructured":"G. Gonthier, J.J. L\u00e9vy and P.-A. Melli\u00e8s (1992), An abstract standardization theorem, in Proceedings of Logic in Computer Science, pp. 72\u201381."},{"key":"27_CR10","unstructured":"J.-Y. Girard et al. (1989), Proofs and types, Cambridge Press, 176 pp."},{"key":"27_CR11","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1017\/S0956796800001106","volume":"4","author":"G. Huet","year":"1994","unstructured":"G\u00e9rard Huet (1994), Residual Theory in \u03bb-Calculus: A Formal Development, Journal of Functional Programming Vol. 4, pp. 371\u2013394.","journal-title":"Journal of Functional Programming"},{"key":"27_CR12","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1090\/S0002-9947-1978-0489603-9","volume":"210","author":"J.R. Hindley","year":"1978","unstructured":"J.R. Hindley (1978), Reductions of residuals are finite, Trans. Amer. Math. Soc. 210, pp. 345\u2013361.","journal-title":"Trans. Amer. Math. Soc."},{"issue":"3","key":"27_CR13","doi-asserted-by":"crossref","first-page":"493","DOI":"10.2307\/2273417","volume":"45","author":"W. Howard","year":"1980","unstructured":"W. Howard (1980), Ordinal analysis of terms of finite type, Journal of Symbolic Logic, 45(3):493\u2013504.","journal-title":"Journal of Symbolic Logic"},{"key":"27_CR14","unstructured":"J.M.E. Hyland (1973), A simple proof of the Church-Rosser theorem, Typescript, Oxford University, 7 pp."},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Stefan Kahrs (1995), Towards a Domain Theory for Termination Proofs, Laboratory for Foundation of Computer Science, 95-314, Department of Computer Science, The University of Edinburgh.","DOI":"10.1007\/3-540-59200-8_60"},{"key":"27_CR16","unstructured":"J.W. Klop (1980), Combinatory reduction systems, Ph.D. thesis, CWI, Amsterdam, Mathematical center tracts, No. 127."},{"key":"27_CR17","unstructured":"J.-J. L\u00e9vy (1978), R\u00e9ductions correctes et optimales dans le lambda calcul, Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII."},{"key":"27_CR18","first-page":"131","volume":"88","author":"G.E. Mints","year":"1979","unstructured":"G.E. Mints (1979), A primitive recursive bound of strong normalization for predicate calculus (in Russian with English abstract), Zapiski Naucnyh Seminarov Leningradskogo Otdelenija Matematiceskogo Instituta im V.A. Steklova Akademii Nauk SSSR (LOMI) 88, pp. 131\u2013135.","journal-title":"Zapiski Naucnyh Seminarov Leningradskogo Otdelenija Matematiceskogo Instituta im V.A. Steklova Akademii Nauk SSSR (LOMI)"},{"key":"27_CR19","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1002\/malq.19790250104","volume":"25","author":"G. Mitschke","year":"1979","unstructured":"G. Mitschke (1979), The standardization theorem for the \u03bb-calculus, Z. Math. Logik Grundlag. Math. 25, pp. 29\u201331.","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"27_CR20","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/BFb0014064","volume":"902","author":"J. Pol van de","year":"1994","unstructured":"J. van de Pol (1994), Strict functionals for termination proofs, Lecture Notes in Computer Science 902, edited by J. Heering, pp. 350\u2013364.","journal-title":"Lecture Notes in Computer Science"},{"key":"27_CR21","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Richard Statman (1979), The typed A-calculus is not elementary, Theoretical Computer Science 9, pp. 73\u201381.","journal-title":"Theoretical Computer Science"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"H. Schwichtenberg (1982), Complexity of normalization in the pure typed lambda-calculus, The L.E.J. Brouwer Centenary Symposium, edited by A.S. Troelstra and D. van Dalen, North-Holland publishing company, pp. 453\u2013457.","DOI":"10.1016\/S0049-237X(09)70143-0"},{"key":"27_CR23","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01621476","volume":"30","author":"H. Schwichtenberg","year":"1991","unstructured":"H. Schwichtenberg (1991), An upper bound for reduction sequences in the typed lambda-calculus, Archive for Mathematical Logic, 30:405\u2013408.","journal-title":"Archive for Mathematical Logic"},{"key":"27_CR24","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Masako Takahashi (1995), Parallel Reductions in \u03bb-Calculus, Information and Computation 118, pp. 120\u2013127.","journal-title":"Information and Computation"},{"issue":"3","key":"27_CR25","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C.P. Wadsworth","year":"1976","unstructured":"C.P. Wadsworth (1976), The relation between computational and denotationa J properties for Scott's D \u221e-models of \u03bb-calculus, SIAM Journal of Computing, 5(3):488\u2013521.","journal-title":"SIAM Journal of Computing"},{"key":"27_CR26","unstructured":"H. Xi (1996), An induction measure on \u03bb-terms and its applications, Technical report 96-192, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh."},{"key":"27_CR27","unstructured":"H. Xi (1996), Separating developments in \u03bb-calculus, Manuscripts."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63385-5_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:25Z","timestamp":1605647905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63385-5_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633853","9783540698067"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-63385-5_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}