{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:15:15Z","timestamp":1770272115495,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198045","type":"print"},{"value":"9783642198052","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19805-2_7","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T09:05:14Z","timestamp":1300093514000},"page":"88-107","source":"Crossref","is-referenced-by-count":13,"title":["Complexity of Strongly Normalising \u03bb-Terms via Non-idempotent Intersection Types"],"prefix":"10.1007","author":[{"given":"Alexis","family":"Bernadet","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theoret. Comput. Sci.\u00a0111, 3\u201357 (1993)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"1993","unstructured":"Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 75\u201390. Springer, Heidelberg (1993)"},{"issue":"4","key":"7_CR3","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. of Symbolic Logic\u00a048(4), 931\u2013940 (1983)","journal-title":"J. of Symbolic Logic"},{"key":"7_CR4","first-page":"213","volume":"265","author":"A. Bucciarelli","year":"2010","unstructured":"Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Categorical models for simply typed resource calculi. ENTCS\u00a0265, 213\u2013230 (2010)","journal-title":"ENTCS"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. CoRR, cs.LO\/0312015 (2003)","DOI":"10.1007\/978-3-540-24727-2_4"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-44904-3_5","volume-title":"Typed Lambda Calculi and Applications","author":"G. Boudol","year":"2003","unstructured":"Boudol, G.: On strong normalization in the intersection type discipline. In: Hofmann, M. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 60\u201374. Springer, Heidelberg (2003)"},{"key":"7_CR7","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 und Grundlagenforschung\u00a019, 139\u2013156 (1978)","journal-title":"Archiv f\u00fcr mathematische Logik und Grundlagenforschung"},{"issue":"4","key":"7_CR8","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame J. of Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. of Formal Logic"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Coquand, T., Spiwack, A.: A proof of strong normalisation using domain theory. Logic. Methods Comput. Science 3(4) (2007)","DOI":"10.2168\/LMCS-3(4:12)2007"},{"key":"7_CR10","first-page":"133","volume":"136","author":"D. Carvalho de","year":"2005","unstructured":"de Carvalho, D.: Intersection types for light affine lambda calculus. ENTCS\u00a0136, 133\u2013152 (2005)","journal-title":"ENTCS"},{"key":"7_CR11","unstructured":"de Carvalho, D.: Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs\/0905.4251 (2009)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/3-540-44612-5_26","volume-title":"Mathematical Foundations of Computer Science 2000","author":"M. Dezani-Ciancaglini","year":"2000","unstructured":"Dezani-Ciancaglini, M., Honsell, F., Motohama, Y.: Compositional characterizations of lambda-terms using intersection types (extended abstract). In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, p. 304. Springer, Heidelberg (2000)"},{"key":"7_CR13","series-title":"ENTCS","first-page":"19","volume-title":"Logic, Model and Computer Science","author":"M. Dezani-Ciancaglini","year":"2007","unstructured":"Dezani-Ciancaglini, M., Tatsuta, M.: A Behavioural Model for Klop\u2019s Calculus. In: Corradini, F., Toffalori, C. (eds.) Logic, Model and Computer Science. ENTCS, vol.\u00a0169, pp. 19\u201332. Elsevier, Amsterdam (2007)"},{"issue":"1-3","key":"7_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(03)00392-X","volume":"309","author":"T. Ehrhard","year":"2003","unstructured":"Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoret. Comput. Sci.\u00a0309(1-3), 1\u201341 (2003)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1305\/ndjfl\/1040067315","volume":"37","author":"S. Ghilezan","year":"1996","unstructured":"Ghilezan, S.: Strong normalization and typability with intersection types. Notre Dame J. Formal Loigc\u00a037(1), 44\u201352 (1996)","journal-title":"Notre Dame J. Formal Loigc"},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoret. Comput. Sci.\u00a050(1), 1\u2013101 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-74915-8_21","volume-title":"Computer Science Logic","author":"M. Gaboardi","year":"2007","unstructured":"Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for lambda -calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"key":"7_CR18","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":"7_CR19","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":"7_CR20","unstructured":"Klop, J.-W.: Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, PhD Thesis (1980)"},{"key":"7_CR21","first-page":"161","volume-title":"Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL 1999)","author":"A.J. Kfoury","year":"1999","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: Proc. of the 26th Annual ACM Symp. on Principles of Programming Languages (POPL 1999), pp. 161\u2013174. ACM Press, New York (1999)"},{"issue":"1-2","key":"7_CR22","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","volume":"318","author":"Y. Lafont","year":"2004","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. Theoret. Comput. Sci.\u00a0318(1-2), 163\u2013180 (2004)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"7_CR23","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","volume":"44","author":"D. Leivant","year":"1986","unstructured":"Leivant, D.: Typing and computational properties of lambda expressions. Theoretical Computer Science\u00a044(1), 51\u201368 (1986)","journal-title":"Theoretical Computer Science"},{"key":"7_CR24","unstructured":"Lengrand, S.: Induction principles as the foundation of the theory of normalisation: Concepts and techniques. Technical report, PPS laboratory, Universit\u00e9 Paris 7 (March 2005), \n                    \n                      http:\/\/hal.ccsd.cnrs.fr\/ccsd-00004358"},{"key":"7_CR25","unstructured":"Lengrand, S.: Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Univ. Paris 7 & Univ. of St Andrews (2006)"},{"key":"7_CR26","first-page":"138","volume-title":"Proc. of the ACM International Conference on Functional Programming","author":"P.M. Neergaard","year":"2004","unstructured":"Neergaard, P.M., Mairson, H.G.: Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In: Okasaki, C., Fisher, K. (eds.) Proc. of the ACM International Conference on Functional Programming, pp. 138\u2013149. ACM Press, New York (September 2004)"},{"key":"7_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."},{"issue":"7","key":"7_CR28","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s001530000070","volume":"40","author":"S. Valentini","year":"2001","unstructured":"Valentini, S.: An elementary proof of strong normalization for intersection types. Arch. Math. Log.\u00a040(7), 475\u2013488 (2001)","journal-title":"Arch. Math. Log."},{"issue":"1","key":"7_CR29","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. Bakel van","year":"1992","unstructured":"van Bakel, S.: Complete restrictions of the intersection type discipline. Theoret. Comput. Sci.\u00a0102(1), 135\u2013163 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"7_CR30","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":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. (ed.) TLCA 1997. LNCS, vol.\u00a01210, pp. 390\u2013404. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19805-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T07:09:31Z","timestamp":1558422571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19805-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198045","9783642198052"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19805-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}