{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:58Z","timestamp":1725489358207},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540734475"},{"type":"electronic","value":"9783540734499"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73449-9_20","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T12:49:53Z","timestamp":1187009393000},"page":"257-272","source":"Crossref","is-referenced-by-count":3,"title":["Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi"],"prefix":"10.1007","author":[{"given":"Kentaro","family":"Kikuchi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. J. Funct. Program.\u00a01, 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Log.\u00a048, 931\u2013940 (1983)","journal-title":"J. Symb. Log."},{"key":"20_CR3","unstructured":"Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology (1997)"},{"key":"20_CR4","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. Theor. Comput. Sci.\u00a0211, 375\u2013395 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR5","unstructured":"Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: Proceedings of CSN 1995 (Computing Science in the Netherlands), pp. 62\u201372 (1995)"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1017\/S0960129500003248","volume":"11","author":"E. Bonelli","year":"2001","unstructured":"Bonelli, E.: Perpetuality in a named lambda calculus with explicit substitutions. Math. Structures Comput. Sci.\u00a011, 47\u201390 (2001)","journal-title":"Math. Structures Comput. Sci."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of ICFP 2000, pp. 233\u2013243 (2000)","DOI":"10.1145\/351240.351262"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci.\u00a017, 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1017\/S0960129502003821","volume":"13","author":"D. Dougherty","year":"2003","unstructured":"Dougherty, D., Lescanne, P.: Reductions, intersection types, and explicit substitutions. Math. Structures Comput. Sci.\u00a013, 55\u201385 (2003)","journal-title":"Math. Structures Comput. Sci."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in a language with control operators. In: Proceedings of PPDP 2004, pp. 155\u2013166 (2004)","DOI":"10.1145\/1013963.1013982"},{"key":"20_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. Log. Comput.\u00a013, 689\u2013706 (2003)","journal-title":"J. Log. Comput."},{"key":"20_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 \u03bb-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":"20_CR13","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 the \u03bb-calculus. Inform. and Comput.\u00a0205, 419\u2013473 (2007)","journal-title":"Inform. and Comput."},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/3-540-45127-7_11","volume-title":"Rewriting Techniques and Applications","author":"Z. Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Uniform normalisation beyond orthogonality. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 122\u2013136. Springer, Heidelberg (2001)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/978-3-540-24754-8_18","volume-title":"Functional and Logic Programming","author":"K. Kikuchi","year":"2004","unstructured":"Kikuchi, K.: A direct proof of strong normalization for an extended Herbelin\u2019s calculus. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol.\u00a02998, pp. 244\u2013259. Springer, Heidelberg (2004)"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.ic.2003.09.004","volume":"189","author":"S. Lengrand","year":"2004","unstructured":"Lengrand, S., Lescanne, P., Dougherty, D., Dezani-Ciancaglini, M., van Bakel, S.: Intersection types for explicit substitutions. Inform. and Comput.\u00a0189, 17\u201342 (2004)","journal-title":"Inform. and Comput."},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Typed Lambda Calculi and Applications","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.-A.: Typed \u03bb-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 328\u2013334. Springer, Heidelberg (1995)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-540-24727-2_30","volume-title":"Foundations of Software Science and Computation Structures","author":"E. Polonovski","year":"2004","unstructured":"Polonovski, E.: Strong normalization of \n                  \n                    \n                  \n                  $\\overline{\\lambda}\\mu\\tilde{\\mu}$\n                -calculus with explicit substitutions. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 423\u2013437. Springer, Heidelberg (2004)"},{"key":"20_CR19","first-page":"561","volume-title":"To H.\u00a0B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"G. Pottinger","year":"1980","unstructured":"Pottinger, G.: A type assignment for the strongly normalizable \u03bb-terms. In: To H.\u00a0B.\u00a0Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press, San Diego (1980)"},{"key":"20_CR20","unstructured":"van Raamsdonk, F., Severi, P.: On normalisation. Technical Report CS-R9545, CWI (1995)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73449-9_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:12:33Z","timestamp":1619503953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73449-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540734475","9783540734499"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73449-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}