{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:06:06Z","timestamp":1725505566724},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540784975"},{"type":"electronic","value":"9783540784999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78499-9_27","type":"book-chapter","created":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T23:02:25Z","timestamp":1207090945000},"page":"380-394","source":"Crossref","is-referenced-by-count":1,"title":["Strong Normalisation of Cut-Elimination That Simulates \u03b2-Reduction"],"prefix":"10.1007","author":[{"given":"Kentaro","family":"Kikuchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1\u20132","key":"27_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoret. Comput. Sci.\u00a0236(1\u20132), 133\u2013178 (2000)","journal-title":"Theoret. Comput. Sci."},{"key":"27_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)"},{"issue":"5","key":"27_CR3","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J.: \u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation. J. Funct. Programming\u00a06(5), 699\u2013722 (1996)","journal-title":"J. Funct. Programming"},{"key":"27_CR4","unstructured":"Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Technische Universiteit Eindhoven, IPA Dissertation Series 1997-05 (1997)"},{"issue":"1\u20132","key":"27_CR5","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"R. Bloo","year":"1999","unstructured":"Bloo, R., Geuvers, H.: Explicit substitution: On the edge of strong normalization. Theoret. Comput. Sci.\u00a0211(1\u20132), 375\u2013395 (1999)","journal-title":"Theoret. Comput. Sci."},{"key":"27_CR6","volume-title":"The Calculi of Lambda Conversion","author":"A. Church","year":"1941","unstructured":"Church, A.: The Calculi of Lambda Conversion. Princeton University Press, Princeton (1941)"},{"key":"27_CR7","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"Proc. of the 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000)","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proc. of the 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000), pp. 233\u2013243. ACM Press, New York (2000)"},{"key":"27_CR8","series-title":"London Math. Soc. Lecture Note Ser.","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1017\/CBO9780511629150.011","volume-title":"Proc. of the Work. on Advances in Linear Logic","author":"V. Danos","year":"1995","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Proc. of the Work. on Advances in Linear Logic. London Math. Soc. Lecture Note Ser., vol.\u00a0222, pp. 211\u2013224. Cambridge University Press, Cambridge (1995)"},{"issue":"3","key":"27_CR9","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. J. of Symbolic Logic\u00a062(3), 755\u2013807 (1997)","journal-title":"J. of Symbolic Logic"},{"issue":"1\u20132","key":"27_CR10","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/S0304-3975(98)00138-8","volume":"212","author":"R. Dyckhoff","year":"1999","unstructured":"Dyckhoff, R., Pinto, L.: Permutability of proofs in intuitionistic sequent calculi. Theoret. Comput. Sci.\u00a0212(1\u20132), 141\u2013155 (1999)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"27_CR11","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1093\/logcom\/13.5.689","volume":"13","author":"R. Dyckhoff","year":"2003","unstructured":"Dyckhoff, R., Urban, C.: Strong normalization of Herbelin\u2019s explicit substitution calculus with substitution propagation. J. Logic Comput.\u00a013(5), 689\u2013706 (2003)","journal-title":"J. Logic Comput."},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H. Herbelin","year":"1995","unstructured":"Herbelin, H.: A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 61\u201375. Springer, Heidelberg (1995)"},{"key":"27_CR13","first-page":"479","volume-title":"To H.\u00a0B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.\u00a0B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479\u2013490. Academic Press, London (1980) (reprint of a manuscript written 1969)"},{"key":"27_CR14","unstructured":"Kamin, S., L\u00e9vy, J.-J.: Attempts for generalizing the recursive path orderings. Handwritten paper. University of Illinois (1980)"},{"issue":"4","key":"27_CR15","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/j.ic.2006.08.008","volume":"205","author":"D. Kesner","year":"2007","unstructured":"Kesner, D., Lengrand, S.: Resource operators for \u03bb-calculus. Inform. and Comput.\u00a0205(4), 419\u2013473 (2007)","journal-title":"Inform. and Comput."},{"key":"27_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11916277_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Kikuchi","year":"2006","unstructured":"Kikuchi, K.: On a local-step cut-elimination procedure for the intuitionistic sequent calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 120\u2013134. Springer, Heidelberg (2006)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-73001-9_41","volume-title":"Computation and Logic in the Real World","author":"K. Kikuchi","year":"2007","unstructured":"Kikuchi, K.: Confluence of cut-elimination procedures for the intuitionistic sequent calculus. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol.\u00a04497, pp. 398\u2013407. Springer, Heidelberg (2007)"},{"key":"27_CR18","unstructured":"Kikuchi, K., Lengrand, S.: Strong normalisation of cut-elimination that simulates \u03b2-reduction - long version, http:\/\/www.lix.polytechnique.fr\/~lengrand\/Work\/"},{"key":"27_CR19","unstructured":"Klop, J.-W.: Combinatory Reduction Systems, Mathematical Centre Tracts, PhD Thesis, vol. 127, CWI, Amsterdam (1980)"},{"key":"27_CR20","series-title":"ENTCS","volume-title":"Post-proc. of the 3rd Int. Work. on Reduction Strategies in Rewriting and Programming (WRS 2003)","author":"S. Lengrand","year":"2003","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: Gramlich, B., Lucas, S. (eds.) Post-proc. of the 3rd Int. Work. on Reduction Strategies in Rewriting and Programming (WRS 2003). ENTCS, vol.\u00a086, Elsevier, Amsterdam (2003)"},{"key":"27_CR21","unstructured":"Lengrand, S.: Induction principles as the foundation of the theory of normalisation: concepts and techniques. Technical report, Universit\u00e9 Paris 7 (March 2005), http:\/\/hal.ccsd.cnrs.fr\/ccsd-00004358"},{"key":"27_CR22","unstructured":"Lengrand, S.: Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Universit\u00e9 Paris 7 & University of St. Andrews (2006)"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-73228-0_24","volume-title":"Typed Lambda Calculi and Applications","author":"K. Nakazawa","year":"2007","unstructured":"Nakazawa, K.: An isomorphism between cut-elimination procedure and proof reduction. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 336\u2013350. Springer, Heidelberg (2007)"},{"key":"27_CR24","unstructured":"Nederpelt, R.: Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD thesis, Eindhoven University of Technology (1973)"},{"key":"27_CR25","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"Pottinger, G.: Normalization as a homomorphic image of cut-elimination. Ann. of Math. Logic\u00a012, 323\u2013357 (1977)","journal-title":"Ann. of Math. Logic"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/3-540-45022-X_51","volume-title":"Automata, Languages and Programming","author":"J.E. Santo","year":"2000","unstructured":"Santo, J.E.: Revisiting the correspondence between cut elimination and normalisation. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 600\u2013611. Springer, Heidelberg (2000)"},{"key":"27_CR27","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1996.2622","volume":"37","author":"M.H.B. S\u00f8rensen","year":"1997","unstructured":"S\u00f8rensen, M.H.B.: Strong normalization from weak normalization in typed lambda-calculi. Inform. and Comput.\u00a037, 35\u201371 (1997)","journal-title":"Inform. and Comput."},{"key":"27_CR28","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"M.H.B. S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H.B., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol.\u00a0149. Elsevier, Amsterdam (2006)"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen, M.H.B., Urzyczyn, P.: Strong cut-elimination in sequent calculus using Klop\u2019s \u03b9-translation and perpetual reduction (available from the authors) (submitted for publication, 2007)","DOI":"10.2178\/jsl\/1230396755"},{"key":"27_CR30","series-title":"Cambridge Tracts in Theoret. Comput. Sci.","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoret. Comput. Sci., vol.\u00a043. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"27_CR31","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge (2000)"},{"key":"27_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-48959-2_26","volume-title":"Typed Lambda Calculi and Applications","author":"C. Urban","year":"1999","unstructured":"Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol.\u00a01581, pp. 365\u2013380. Springer, Heidelberg (1999)"},{"issue":"2","key":"27_CR33","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/inco.1998.2750","volume":"149","author":"F. Raamsdonk van","year":"1999","unstructured":"van Raamsdonk, F., Severi, P., S\u00f8rensen, M.H.B., Xi, H.: Perpetual reductions in \u03bb-calculus. Inform. and Comput.\u00a0149(2), 173\u2013225 (1999)","journal-title":"Inform. and Comput."},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-62688-3_48","volume-title":"Typed Lambda Calculi and Applications","author":"H. Xi","year":"1997","unstructured":"Xi, H.: Weak and strong beta normalisations in typed lambda-calculi. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol.\u00a01210, pp. 390\u2013404. Springer, Heidelberg (1997)"},{"key":"27_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"Zucker, J.: The correspondence between cut-elimination and normalization. Ann. of Math. Logic\u00a07, 1\u2013156 (1974)","journal-title":"Ann. of Math. Logic"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78499-9_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T11:31:45Z","timestamp":1684323105000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78499-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540784975","9783540784999"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78499-9_27","relation":{},"subject":[]}}