{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T18:23:06Z","timestamp":1761848586365,"version":"build-2065373602"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1023\/a:1025693307470","type":"journal-article","created":{"date-parts":[[2003,9,23]],"date-time":"2003-09-23T22:47:08Z","timestamp":1064357228000},"page":"253-285","source":"Crossref","is-referenced-by-count":4,"title":["Strong Normalization from Weak Normalization by Translation into the Lambda-I-Calculus"],"prefix":"10.1007","volume":"16","author":[{"given":"Inge Li","family":"G\u00f8rtz","sequence":"first","affiliation":[]},{"given":"Signe","family":"Reuss","sequence":"additional","affiliation":[]},{"given":"Morten Heine","family":"S\u00f8rensen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5142638_CR1","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P. Lambda calculi with types. In Handbook of Logic in Computer Science, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum (Eds.). Oxford University Press, 1992, Vol. II, pp. 117\u2013309.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"5142638_CR2","unstructured":"Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, 2nd revised edition. North-Holland, 1984."},{"key":"5142638_CR3","doi-asserted-by":"crossref","unstructured":"de Groote, P. The conservation theorem revisited. In Typed Lambda Calculus and Applications, M. Bezem and J.F. Groote (Eds.). Vol. 664 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 163\u2013178.","DOI":"10.1007\/BFb0037105"},{"key":"5142638_CR4","unstructured":"Gandy, R.O. Proofs of strong normalization. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press Limited, 1980, pp. 457\u2013477."},{"key":"5142638_CR5","unstructured":"Girard, J.-Y. Proof Theory and Logical Complexity, Bibliopolis, 1987, Vol. 1."},{"key":"5142638_CR6","unstructured":"G\u00f8rtz, I. and Nielsen, S. Functional interpretations and normalization. Report, Department of Computer Science, University of Copenhagen, March 1999."},{"issue":"3","key":"5142638_CR7","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1017\/S0956796897002748","volume":"7","author":"J. Hatcliff","year":"1997","unstructured":"Hatcliff, J. and Danvy, O. Thunks and the lambda-calculus. Journal of Functional Programming, 7(3) (1997) 303\u2013319.","journal-title":"Journal of Functional Programming"},{"key":"5142638_CR8","doi-asserted-by":"crossref","unstructured":"Karr, M. \u201cDelayability\u201d in proofs of strong normalizability in the typed lambda calculus. In Mathematical Foundations of Computer Software, H. Ehrig, C. Floyd, M. Nivat and J. Thatcher (Eds.). Vol. 185 of Lecture Notes in Computer Science, Springer-Verlag, 1985, pp. 208\u2013222.","DOI":"10.1007\/3-540-15198-2_13"},{"key":"5142638_CR9","unstructured":"Kfoury, A.J. and Wells, J. New notions of reduction and non-semantic proofs of \u03b2-strong normalization in typed \u03bb-calculi. Technical Report 94-01, Boston University Computer Science Department, 1994. Also in Logic in Computer Science, 1995."},{"key":"5142638_CR10","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z. Perpetuality and strong normalization in orthogonal term rewriting systems. In Symposium on Theoretical Aspects of Computer Science, P. Enjalbert, E.W. Mayr and K.W. Wagner (Eds.). Vol. 775 of Lecture Notes in Computer Science, Springer-Verlag, 1994, pp. 163\u2013174.","DOI":"10.1007\/3-540-57785-8_139"},{"key":"5142638_CR11","unstructured":"Klop, J.W. Combinatory Reduction Systems. PhD thesis, Utrecht University, Vol. 127 of CWI Tracts, Amsterdam, 1980."},{"key":"5142638_CR12","unstructured":"Loader, R. Normalisation by translation. Presented at the BRA TYPES workshop, Turin. See also www.dcs.ed.ac.uk\/~loader., 1995."},{"key":"5142638_CR13","doi-asserted-by":"crossref","unstructured":"Nederpelt, R. Strong Normalization for a Typed Lambda Calculus with Lambda Structured Types. PhD thesis, Eindhoven, 1973. Reprinted as pp. 389\u2013468 of [14].","DOI":"10.1016\/S0049-237X(08)70217-9"},{"key":"5142638_CR14","volume-title":"Selected Papers on Automath","author":"R. Nederpelt","year":"1994","unstructured":"Nederpelt, R., Geuvers, H., and de Vrijer, R.C. Selected Papers on Automath. North-Holland, Amsterdam, 1994."},{"key":"5142638_CR15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G. Call-by-name, call-by-value and the \u03bb-calculus. Theoretical Computer Science, 1 (1975) 125\u2013159.","journal-title":"Theoretical Computer Science"},{"key":"5142638_CR16","unstructured":"van de Pol, J. Termination of Higher-Order Rewrite Systems. PhD thesis, University of Utrecht, 1996. Vol. 16 of Questiones Infinitae."},{"issue":"1","key":"5142638_CR17","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1996.2622","volume":"133","author":"M.H. S\u00f8rensen","year":"1997","unstructured":"S\u00f8rensen, M.H. Strong normalization from weak normalization in typed \u03bb-calculi. Information and Computation, 133(1) (1997) 35\u201371.","journal-title":"Information and Computation"},{"issue":"2","key":"5142638_CR18","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1006\/inco.1998.2750","volume":"149","author":"F. van Raamsdonk","year":"1999","unstructured":"van Raamsdonk, F., Severi, P., S\u00f8rensen, M.H., and Xi, H. Perpetual reductions in \u03bb-calculus. Information and Computation, 149(2) (1999) 173\u2013225.","journal-title":"Information and Computation"},{"key":"5142638_CR19","doi-asserted-by":"crossref","unstructured":"de Vrijer, R.C. Exactly estimating functionals and strong normalization. Koninklijke Nederlandse Akademie van wetenschappen, 90(4) (1987). Also appeared as [20].","DOI":"10.1016\/1385-7258(87)90012-6"},{"key":"5142638_CR20","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1016\/1385-7258(87)90012-6","volume":"49","author":"R.C. de Vrijer","year":"1987","unstructured":"de Vrijer, R.C. Exactly estimating functionals and strong normalization. Indagationes Mathematicae, 49 (1987) 479\u2013493.","journal-title":"Indagationes Mathematicae"},{"key":"5142638_CR21","unstructured":"Xi, H. On weak and strong normalization. Research Report 96\u2013187, Department of Mathematical Science, Carnegie Mellon University, 1996. See also www.cse.ogi.edu\/~hongwei."},{"key":"5142638_CR22","doi-asserted-by":"crossref","unstructured":"Xi, H. Weak and strong beta normalisations in typed \u03bb-calculi. In Typed Lambda Calculus and Applications, P. de Groote and J.R. Hindley (Eds.). Vol. 1210 of Lecture Notes in Computer Science, Springer-Verlag, 1997, pp. 390\u2013404.","DOI":"10.1007\/3-540-62688-3_48"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025693307470.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1025693307470\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025693307470.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:43:57Z","timestamp":1751982237000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1025693307470"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5142638"],"URL":"https:\/\/doi.org\/10.1023\/a:1025693307470","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}