{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:12Z","timestamp":1759638972740},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642232824"},{"type":"electronic","value":"9783642232831"}],"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-23283-1_10","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T02:30:27Z","timestamp":1314153027000},"page":"116-134","source":"Crossref","is-referenced-by-count":1,"title":["Intersection Types for the Resource Control Lambda Calculi"],"prefix":"10.1007","author":[{"given":"Silvia","family":"Ghilezan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jelena","family":"Iveti\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvia","family":"Likavec","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1&2","key":"10_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. Theor. Comput. Sci.\u00a0111(1&2), 3\u201357 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR2","doi-asserted-by":"publisher","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, UK (1998)"},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Inform. Comput.\u00a0125(2), 103\u2013117 (1996)","journal-title":"Inform. Comput."},{"key":"10_CR4","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984), revised edition"},{"key":"10_CR5","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"1992","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117\u2013309. Oxford University Press, UK (1992)"},{"issue":"4","key":"10_CR6","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Logic\u00a048(4), 931\u2013940 (1984) (1983)","journal-title":"J. Symb. Logic"},{"key":"10_CR7","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)"},{"key":"10_CR8","unstructured":"Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: Computer Science in the Netherlands, CSN 1995, pp. 62\u201372 (1995)"},{"key":"10_CR9","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"},{"issue":"4","key":"10_CR10","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. Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. Formal Logic"},{"key":"10_CR11","first-page":"233","volume-title":"5th International Conference on Functional Programming, ICFP 2000","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: 5th International Conference on Functional Programming, ICFP 2000, pp. 233\u2013243. ACM Press, New York (2000)"},{"issue":"1-3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.tcs.2004.01.023","volume":"316","author":"M. Dezani-Ciancaglini","year":"2004","unstructured":"Dezani-Ciancaglini, M., Ghilezan, S., Likavec, S.: Behavioural Inverse Limit Models. Theor. Comput Sci.\u00a0316(1-3), 49\u201374 (2004)","journal-title":"Theor. Comput Sci."},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1016\/j.tcs.2008.01.022","volume":"398","author":"D.J. Dougherty","year":"2008","unstructured":"Dougherty, D.J., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. Theor. Comput Sci.\u00a0398, 114\u2013128 (2008)","journal-title":"Theor. Comput Sci."},{"key":"10_CR14","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":"10_CR15","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J., Iveti\u0107, J., Likavec, S.: Characterising strongly normalising intuitionistic terms. Fundamenta Informaticae (to appear 2011)","DOI":"10.3233\/FI-2012-772"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0168-0072(97)00047-X","volume":"91","author":"J. Gallier","year":"1998","unstructured":"Gallier, J.: Typing untyped \u03bb-terms, or reducibility strikes again! Ann. Pure Appl. Logic\u00a091, 231\u2013270 (1998)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"10_CR17","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 Logic\u00a037(1), 44\u201352 (1996)","journal-title":"Notre Dame J. Formal Logic"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22303-7_7","volume-title":"8th International Tbilisi Symposium on Language, Logic and Computation","author":"S. Ghilezan","year":"2011","unstructured":"Ghilezan, S., Iveti\u0107, J., Lescanne, P., \u017duni\u0107, D.: Intuitionistic sequent-style calculus with explicit structural rules. In: Bezhanishvili, N. (ed.) TbiLLC 2009. LNCS, vol.\u00a06618, pp. 101\u2013124. Springer, Heidelberg (2011)"},{"key":"10_CR19","unstructured":"Ghilezan, S., Likavec, S.: Computational interpretations of logics. In: Ognjanovi\u0107, Z. (ed.) Collection of Papers, Special issue Logic in Computer Science, vol. 20(12), pp. 159\u2013215. Mathematical Institute of Serbian Academy of Sciences and Arts (2009)"},{"key":"10_CR20","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":"10_CR21","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulas-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, London (1980)"},{"issue":"4","key":"10_CR22","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 lambda-calculus. Inform. Comput.\u00a0205(4), 419\u2013473 (2007)","journal-title":"Inform. Comput."},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-642-03816-7_40","volume-title":"Mathematical Foundations of Computer Science 2009","author":"D. Kesner","year":"2009","unstructured":"Kesner, D., Renaud, F.: The prismoid of resources. In: Kr\u00e1lovi\u010d, R., Niwi\u0144ski, D. (eds.) MFCS 2009. LNCS, vol.\u00a05734, pp. 464\u2013476. Springer, Heidelberg (2009)"},{"key":"10_CR24","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":"10_CR25","unstructured":"Matthes, R.: Characterizing strongly normalizing terms of a \u03bb-calculus with generalized applications via intersection types. In: Hindley, J.R., et al. (eds.) ICALP Workshops 2000. Carleton Scientific (2000)"},{"issue":"5","key":"10_CR26","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1017\/S0956796805005587","volume":"15","author":"P.M. Neergaard","year":"2005","unstructured":"Neergaard, P.M.: Theoretical pearls: A bargain for intersection types: a simple strong normalization proof. J. Funct. Program.\u00a015(5), 669\u2013677 (2005)","journal-title":"J. Funct. Program."},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-642-12032-9_25","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Pagani","year":"2010","unstructured":"Pagani, M., della Rocca, S.R.: Solvability in resource lambda-calculus. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 358\u2013373. Springer, Heidelberg (2010)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"10_CR29","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)"},{"issue":"2","key":"10_CR30","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"126","author":"L. Regnier","year":"1994","unstructured":"Regnier, L.: Une \u00e9quivalence sur les lambda-termes. Theor. Comput Sci.\u00a0126(2), 281\u2013292 (1994)","journal-title":"Theor. Comput Sci."},{"key":"10_CR31","unstructured":"Rose, K.H.: CRSX - Combinatory Reduction Systems with Extensions. In: Schmidt-Schau\u00df, M. (ed.) 22nd International Conference on Rewriting Techniques and Applications, RTA 2011. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a010, pp. 81\u201390. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2011)"},{"key":"10_CR32","unstructured":"Rose, K.H.: Implementation Tricks That Make CRSX Tick. Talk at IFIP 1.6 Workshop, RDP 2011 (May 2011)"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"10_CR34","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537779.001.0001","volume-title":"Substructural Logics","author":"P. Schroeder-Heister","year":"1993","unstructured":"Schroeder-Heister, P., Do\u0161en, K.: Substructural Logics. Oxford University Press, UK (1993)"},{"key":"10_CR35","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symb. Logic\u00a032, 198\u2013212 (1967)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"10_CR36","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. Theor. Comput Sci.\u00a0102(1), 135\u2013163 (1992)","journal-title":"Theor. Comput Sci."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23283-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,10]],"date-time":"2024-04-10T13:05:34Z","timestamp":1712754334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23283-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642232824","9783642232831"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23283-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}