{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:07:58Z","timestamp":1751983678277},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:49:02Z","timestamp":1330278542000},"page":"390-404","source":"Crossref","is-referenced-by-count":10,"title":["Weak and strong beta normalisations in typed \u03bb-calculi"],"prefix":"10.1007","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"24_CR1","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":"24_CR2","first-page":"117","volume-title":"Handbook of Logic in Computer Science Vol. 2","author":"H.P. Barendregt","year":"1992","unstructured":"H.P. Barendregt (1992), Lambda calculi with types, in Handbook of Logic in Computer Science Vol. 2, edited by S. Abramsky, D. M. Gabbay and T.S.E. Maibaum, Clarendon Press, Oxford, pp. 117\u2013309."},{"key":"24_CR3","first-page":"403","volume":"18","author":"J.A. Bergstra","year":"1982","unstructured":"J.A. Bergstra and J.W. Klop (1982), Strong normalization and perpetual reductions in the lambda calculus, J. Inform. Process. Cybernet. 18, pp. 403\u2013417.","journal-title":"J. Inform. Process. Cybernet."},{"key":"24_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":"24_CR5","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand and G. Hu\u00e9t (1988), The calculus of constructions, Information and Computation vol. 76, pp. 95\u2013120.","journal-title":"Information and Computation"},{"issue":"4","key":"24_CR6","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo and M. Dezani-Ciancaglini (1980), An extension of basic functionality theory for the lambda-calculus, Notre Dame Journal of Formal Logic 21 (4), pp. 685\u2013693.","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"1","key":"24_CR7","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/malq.19810270205","volume":"27","author":"M. Coppo","year":"1981","unstructured":"M. Coppo, M. Dezani-Ciancaglini and B. Venneri (1981), Functional characters of solvable terms, Zeit. Math. Logik und Grundlagen der Math. 27 (1), pp. 45\u201358.","journal-title":"Zeit. Math. Logik und Grundlagen der Math."},{"key":"24_CR8","unstructured":"P. de Groote (1993), The conservation theorem revisited, Typed Lambda Calculi and Applications: TLCA'93, LNCS vol. 664, Springer, pp. 163\u2013178."},{"key":"24_CR9","unstructured":"R.O. Gandy (1980), An early proof of normalisation by A.M. Turing, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 453\u2013456."},{"key":"24_CR10","unstructured":"R.O. Gandy (1980), Proofs of strong normalisation, in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 457\u2013478."},{"key":"24_CR11","unstructured":"J.-Y. Girard (1972), Interpr\u00e9tation Fonctionnelle et \u00c9limination des Coupures de l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur, Th\u00e8se de Doctorat d'Etat, Universit\u00e9 Paris VII."},{"key":"24_CR12","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.J. Nederhof (1991), A modular proof of strong normalisation for the calculus of constructions, J. Functional Programming 1, 155\u2013189.","journal-title":"J. Functional Programming"},{"key":"24_CR13","first-page":"194","volume-title":"A framework for defining logics","author":"R. Harper","year":"1987","unstructured":"R. Harper, F. Honsell and G. Plotkin (1987), A framework for defining logics. In Proc. Second Annual Symposium on Logic in Computer Science, I.E.E.E., Ithaca, N.Y., pages 194\u2013204."},{"key":"24_CR14","unstructured":"R. Harper and M. Lillibridge (1993), Explicit polymorphism and CPS conversion, In Proceedings of the Twentieth ACM Symposium on Principles of Programming Languages, pp. 206\u2013209"},{"issue":"34","key":"24_CR15","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF01019463","volume":"6","author":"R. Harper","year":"1993","unstructured":"R. Harper and M. Lillibridge (1993), Polymorphic type assignment and CPS conversion, LISP and Symbolic Computation, vol. 6, 3(4), pp. 361\u2013380.","journal-title":"LISP and Symbolic Computation"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Stefan Kahrs (1995), Towards a Domain Theory for Termination Proofs, Laboratory for Foundation of Computer Science, Report 95-314, Department of Computer Science, The University of Edinburgh.","DOI":"10.1007\/3-540-59200-8_60"},{"key":"24_CR17","unstructured":"M. Karr (1985), \u201cDelayability\u201d in proofs of strong normalisabilities in the typed lambda-calculus, in Mathematical Foundation of Computer Software, edited by H. Ehrig, C. Floyd, M. N\u00efvat and J. Thatcher, LNCS vol. 185, Springer, pp. 208\u2013222."},{"key":"24_CR18","series-title":"Mathematical Center Tracts, No. 127","volume-title":"Ph.D. thesis","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop (1980), Combinatory Reduction Systems, Ph.D. thesis, CWI, Amsterdam, Mathematical Center Tracts, No. 127."},{"key":"24_CR19","first-page":"1","volume-title":"Handbook of Logic in Computer Science Vol.2","author":"J.W. Klop","year":"1992","unstructured":"J.W. Klop, (1992), Term rewriting systems, in Handbook of Logic in Computer Science Vol.2, edited by S. Abramsky, D. M. Gabbay and T.S.E. Maibaum, Clarendon Press, Oxford, pp. 1\u2013116."},{"key":"24_CR20","volume-title":"Lambda-calcul, Types et Mod\u00e8les","author":"J.L. Krivine","year":"1990","unstructured":"J.L. Krivine (1990), Lambda-calcul, Types et Mod\u00e8les, Masson, Paris."},{"key":"24_CR21","unstructured":"A.J. Kfoury and J.B. Wells (1994), New notions of reduction and non-semantic proofs of \u03b2-strong normalisation in typed \u03bb-calculi, Tech. Rep. 94-104, Computer Science Department, Boston University."},{"key":"24_CR22","unstructured":"R.P. Nederpelt (1973), Strong normalization in a typed lambda calculus with lambda structured types, Ph.D. thesis, Technische Hogeschool Eindhoven."},{"key":"24_CR23","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"G. Plotkin (1975), Call-by-name, call-by-value, and the lambda calculus, Theoretical Computer Science, vol 1, pp. 125\u2013159.","journal-title":"Theoretical Computer Science"},{"key":"24_CR24","unstructured":"J. van de Pol (1994), Termination proofs for higher-order rewrite systems, in Higher Order Algebra, Logic and Term Rewriting, edited by J. Heering, K. Meinke, B. M\u00f6ller and T. Nipkow, LNCS vol. 816, Springer, pp. 305\u2013325."},{"key":"24_CR25","unstructured":"J. van de Pol and H. Schwichtenberg (1995), Strict functionals for termination proofs, Typed lambda calculi and applications: TLCA '95, LNCS vol. 902, Springer, pp. 350\u2013364."},{"key":"24_CR26","volume-title":"Natural Deduction: A proof theoretical study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz (1965), Natural Deduction: A proof theoretical study, Almquist & Wiksell publishing company, Stockholm."},{"key":"24_CR27","volume-title":"Proceedings of the 2nd Scandinavian Logic Symposium","author":"D. Prawitz","year":"1971","unstructured":"D. Prawitz (1971), Ideas and results of proof theory, in Proceedings of the 2nd Scandinavian Logic Symposium, edited by J.E. Fenstad, North-Holland Publishing Company, Amsterdam."},{"key":"24_CR28","unstructured":"J. Reynolds (1974), Towards a theory of type structure, Colloquium sur la Programmation, LNCS vol. 19, Springer, pp. 408\u2013423."},{"key":"24_CR29","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":"24_CR30","unstructured":"M.H. S\u00f8rensen (1996), Strong Normalization from Weak Normalization by A-Translation in Typed lambda-Calculi, Manuscript announced on the types mailing list, February."},{"key":"24_CR31","unstructured":"J. Springintveld (1993), Lower and upper bounds for reductions of types in \u03bb\u03c9 and \u03bbP, in Typed lambda calculi and applications: TLCA'93, LNCS vol. 664, Springer, pp. 391\u2013405."},{"key":"24_CR32","unstructured":"P. Urzyczyn (1995), Positive recursive type assignment, in Mathematical Foundations of Computer Science, LNCS vol. 969, Springer, pp. 382\u2013391."},{"key":"24_CR33","volume-title":"Research Report 96-187","author":"H. Xi","year":"1996","unstructured":"H. Xi (1996), On weak and strong normalisations, Research Report 96-187, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh."},{"key":"24_CR34","volume-title":"Research Report 96-189","author":"H. Xi","year":"1996","unstructured":"H. Xi (1996), Upper bounds for standardisations and an application, Research Report 96-189, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh."},{"key":"24_CR35","volume-title":"Research Report 96-192","author":"H. Xi","year":"1996","unstructured":"H. Xi (1996), An induction measure on \u03bb-terms and its applications, Research Report 96-192, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:14:06Z","timestamp":1605629646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}