{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:27Z","timestamp":1725484647273},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434009"},{"type":"electronic","value":"9783540459958"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45995-2_33","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T02:33:34Z","timestamp":1180492414000},"page":"356-370","source":"Crossref","is-referenced-by-count":1,"title":["Characterising Strong Normalisation for Explicit Substitutions"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"issue":"4","key":"33_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"33_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983504","volume-title":"Domains and lambda-calculi","author":"R. M. Amadio","year":"1998","unstructured":"R. M. Amadio and P.-L. Curien. Domains and lambda-calculi. Cambridge University Press, Cambridge, 1998."},{"issue":"1","key":"33_CR3","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. Bakel van","year":"1992","unstructured":"S. van Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science, 102(1):135\u2013163, 1992.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"33_CR4","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","volume":"151","author":"S. Bakel van","year":"1995","unstructured":"S. van Bakel. Intersection Type Assingment Systems. Theoretical Computer Science, 151(2):385\u2013435, 1995.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"33_CR5","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931\u2013940, 1983.","journal-title":"The Journal of Symbolic Logic"},{"issue":"5","key":"33_CR6","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. \u03bbv, a calculus of explicit substitutions which preserves strong normalization. Journal of Functional Programming, 6(5):699\u2013722, 1996.","journal-title":"Journal of Functional Programming"},{"key":"33_CR7","unstructured":"R. Bloo and K. Rose. Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In Computer Science in the Netherlands, pages 62\u201372. Koninklijke Jaarbeurs, 1995."},{"issue":"4","key":"33_CR8","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the \u03bb-calculus. Notre Dame Journal of Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"33_CR9","first-page":"535","volume-title":"To H. B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"M. Coppo","year":"1980","unstructured":"M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and \u03bb-calculus semantics. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 535\u2013560. Academic Press, London, 1980."},{"key":"33_CR10","series-title":"Lect Notes Comput Sci","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":"M. Dezani-Ciancaglini, F. Honsell, and Y. Motohama. Compositional characterization of \u03bb-terms using intersection types. In Mathematical Foundations of Computer Science 2000, volume 1893 of Lecture Notes in Computer Science, pages 304\u2013313. Springer, 2000."},{"key":"33_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45413-6_13","volume-title":"Typed Lambda Calculi and Applications 2001","author":"D. Dougherty","year":"2001","unstructured":"D. Dougherty and P. Lescanne. Reductions, intersection types and explicit substitutions. In Typed Lambda Calculi and Applications 2001, volume 2044 of Lecture Notes in Computer Science, pages 121\u2013135. Springer, 2001."},{"key":"33_CR12","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/S0168-0072(97)00047-X","volume":"91","author":"J. Gallier","year":"1998","unstructured":"J. Gallier. Typing untyped \u03bb-terms, or reducibility strikes again! Annals of Pure and Applied Logic, 91:231\u2013270, 1998.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"33_CR13","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1305\/ndjfl\/1040067315","volume":"37","author":"S. Ghilezan","year":"1996","unstructured":"S. Ghilezan. Strong normalization and typability with intersection types. Notre Dame Journal of Formal Logic, 37(1):44\u201352, 1996.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e1 l\u2019analyse, et son application \u00e1 l\u2019elimination des coupures dans l\u2019analyse et la th\u00e9orie des types. In 2nd Scandinavian Logic Symposium, pages 63\u201392. North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"issue":"4","key":"33_CR15","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1017\/S0956796897002785","volume":"7","author":"F. Kamareddine","year":"1997","unstructured":"F. Kamareddine and A. Rios. Extending a \u03bb-calculus with explicit substitutions which preserves strong normalization into a confluent calculus of open terms. Journal of Functional Programming, 7(4):395\u2013420, 1997.","journal-title":"Journal of Functional Programming"},{"key":"33_CR16","volume-title":"Lambda-calcul Types et mod\u00e8les","author":"J.-L. Krivine","year":"1990","unstructured":"J.-L. Krivine. Lambda-calcul Types et mod\u00e8les. Masson, Paris, 1990."},{"issue":"1","key":"33_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","volume":"44","author":"D. Leivant","year":"1986","unstructured":"D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44(1):51\u201368, 1986.","journal-title":"Theoretical Computer Science"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"S. Lengrand, D. Dougherty, and P. Lescanne, An improved system of intersection types for explicit substitutions, Internal Report, ENS de Lyon, 2001.","DOI":"10.1007\/978-0-387-35608-2_42"},{"key":"33_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Typed Lambda Calculi and Applications 2001","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitution may not terminate. In Typed Lambda Calculi and Applications 2001, volume 902 of Lecture Notes in Computer Science, pages 328\u2013334. Springer, 1995."},{"key":"33_CR20","first-page":"415","volume":"B","author":"J. C. Mitchell","year":"1990","unstructured":"J. C. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, volume B, pages 415\u2013431. Elsevire, Amsterdam, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"33_CR21","unstructured":"J. C. Mitchell. Foundation for Programmimg Languages. MIT Press, 1996."},{"key":"33_CR22","first-page":"561","volume-title":"To H. B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"G. Pottinger","year":"1980","unstructured":"G. Pottinger. A type assignment for the strongly normalizable \u03bb-terms. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 561\u2013577. Academic Press, London, 1980."},{"key":"33_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-48959-2_23","volume-title":"Typed Lambda Calculi and Applications 1999","author":"E. Ritter","year":"1999","unstructured":"E. Ritter. Characterizing explicit substitutions which preserve termination. In Typed Lambda Calculi and Applications 1999, volume 1581 of Lecture Notes in Computer Science, pages 325\u2013339. Springer, 1999."},{"key":"33_CR24","unstructured":"P. Severi. Normalisation in lambda calculus and its relation to type inference. PhD thesis, Eindhoven University of Technology, 1996."},{"key":"33_CR25","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32:198\u2013212, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"W. W. Tait. A realizability interpretation of the theory of species. In Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 240\u2013251. Springer, 1975.","DOI":"10.1007\/BFb0064875"}],"container-title":["Lecture Notes in Computer Science","LATIN 2002: Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45995-2_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T12:30:22Z","timestamp":1556454622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45995-2_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434009","9783540459958"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45995-2_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}