{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:05Z","timestamp":1725511805714},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540680840"},{"type":"electronic","value":"9783540681038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68103-8_6","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T00:10:07Z","timestamp":1210032607000},"page":"85-99","source":"Crossref","is-referenced-by-count":1,"title":["Characterising Strongly Normalising Intuitionistic Sequent Terms"],"prefix":"10.1007","author":[{"given":"J.","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]},{"given":"S.","family":"Ghilezan","sequence":"additional","affiliation":[]},{"given":"J.","family":"Iveti\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511983504","volume-title":"Domains and Lambda-Calculi","author":"R. Amadio","year":"1998","unstructured":"Amadio, R., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, vol.\u00a046. Cambridge University Press, Cambridge (1998)"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H. Barendregt","year":"2000","unstructured":"Barendregt, H., Ghilezan, S.: Lambda terms for natural deduction, sequent calculus and cut elimination. J. Funct. Program.\u00a010(1), 121\u2013134 (2000)","journal-title":"J. Funct. Program."},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BF02011875","volume":"19","author":"M. Coppo","year":"1978","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: A new type-assignment for lambda terms. Archiv f\u00fcr Mathematische Logik\u00a019, 139\u2013156 (1978)","journal-title":"Archiv f\u00fcr Mathematische Logik"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. Theoretical Computer Science (to appear, 2007)","DOI":"10.1016\/j.tcs.2008.01.022"},{"key":"6_CR5","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. Esp\u00edrito Santo","year":"2000","unstructured":"Esp\u00edrito Santo, J.: 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":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-73228-0_10","volume-title":"Typed Lambda Calculi and Applications","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Completing Herbelin\u2019s programme. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 118\u2013132. Springer, Heidelberg (2007)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-73449-9_14","volume-title":"Term Rewriting and Applications","author":"J. Esp\u00edrito Santo","year":"2007","unstructured":"Esp\u00edrito Santo, J.: Delayed substitutions. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 169\u2013183. Springer, Heidelberg (2007)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-44904-3_20","volume-title":"Typed Lambda Calculi and Applications","author":"J. Esp\u00edrito Santo","year":"2003","unstructured":"Esp\u00edrito Santo, J., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculi with cuts. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 286\u2013300. Springer, Heidelberg (2003)"},{"key":"6_CR9","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":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/10721975_10","volume-title":"Rewriting Techniques and Applications","author":"F. Joachimski","year":"2000","unstructured":"Joachimski, F., Matthes, R.: Standardization and confluence for \u039bJ. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 141\u2013155. Springer, Heidelberg (2000)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-540-73449-9_20","volume-title":"Term Rewriting and Applications","author":"K. Kikuchi","year":"2007","unstructured":"Kikuchi, K.: Simple proofs of characterizing strong normalization for explicit substitution calculi. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 257\u2013272. Springer, Heidelberg (2007)"},{"key":"6_CR12","unstructured":"Krivine, J.L.: Lambda-calcul, types et mod\u00e8les, Masson, Paris (1990)"},{"issue":"1","key":"6_CR13","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. Inf. Comput.\u00a0189(1), 17\u201342 (2004)","journal-title":"Inf. Comput."},{"key":"6_CR14","unstructured":"Matthes, R.: Characterizing strongly normalizing terms of a \u03bb-calculus with generalized applications via intersection types. In: Rolin, J., et al. (eds.) ICALP Workshops 2000, pp. 339\u2013354. Carleton Scientific (2000)"},{"key":"6_CR15","first-page":"561","volume-title":"To H. B. Curry: 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: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press, London (1980)"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0304-3975(88)90101-6","volume":"59","author":"S. Ronchi","year":"1988","unstructured":"Ronchi, S., Rocca, D.: Principal type scheme and unification for intersection type discipline. Theor. Comput. Sci.\u00a059, 181\u2013209 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR17","unstructured":"Rose, K.: Explicit substitutions: Tutorial & survey. Technical Report LS-96-3, BRICS (1996)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-08860-1_30","volume-title":"Automata, Languages and Programming","author":"P. Sall\u00e9","year":"1978","unstructured":"Sall\u00e9, P.: Une extension de la th\u00e9orie des types en lambda-calcul. In: Ausiello, G., B\u00f6hm, C. (eds.) ICALP 1978. LNCS, vol.\u00a062, pp. 398\u2013410. Springer, Heidelberg (1978)"},{"issue":"1\u20132","key":"6_CR19","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/S0304-3975(98)00143-1","volume":"212","author":"H. Schwichtenberg","year":"1999","unstructured":"Schwichtenberg, H.: Termination of permutative conversions in intuitionistic Gentzen calculi. Theoretical Computer Science\u00a0212(1\u20132), 247\u2013260 (1999)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68103-8_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:32:54Z","timestamp":1620001974000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68103-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540680840","9783540681038"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68103-8_6","relation":{},"subject":[]}}