{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T03:54:04Z","timestamp":1725767644311},"publisher-location":"Boston, MA","reference-count":21,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781475752755"},{"type":"electronic","value":"9780387356082"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/978-0-387-35608-2_42","type":"book-chapter","created":{"date-parts":[[2013,12,29]],"date-time":"2013-12-29T16:57:25Z","timestamp":1388336245000},"page":"511-523","source":"Crossref","is-referenced-by-count":1,"title":["An Improved System of Intersection Types for Explicit Substitutions"],"prefix":"10.1007","author":[{"given":"Dan","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"42_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., and L\u00e9vy, J.-J. (1991). Explicit substitutions. Journal of Functional Programming, 1 (4): 375\u2013416.","journal-title":"Journal of Functional Programming"},{"key":"42_CR2","first-page":"V","volume-title":"The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier Science Publishers B","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H. P. (1984). The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier Science Publishers B. V. ( North-Holland), Amsterdam. Second edition."},{"issue":"5","key":"42_CR3","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z Benaissa","year":"1996","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P., and Rouyer-Degli, J. (1996). Av, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6 (5): 699\u2013722.","journal-title":"Journal of Functional Programming"},{"key":"42_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. and Geuvers, J. H. (1999). Explicit substitution: on the edge of strong normalization. Theoretical Computer Science, 211: 375\u2013395.","journal-title":"Theoretical Computer Science"},{"key":"42_CR5","first-page":"62","volume-title":"Csn 95\u2014Computing Science in the Netherlands","author":"R Bloo","year":"1995","unstructured":"Bloo, R. and Rose, K. H. (1995). Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In CSN \u201985\u2014Computing Science in the Netherlands, pages 62\u201372, Koninklijke Jaarbeurs, Utrecht."},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"Bucciarelli, A., Lorenzis, S. D., Piperno, A., and Salvo, I. (1999). Some computational properties of intersection types. In 14th Symposium on Logic in Computer Science (LICS\u201999),pages 109\u2013118, Washington \u2014 Brussels \u2014 Tokyo. IEEE.","DOI":"10.1109\/LICS.1999.782598"},{"key":"42_CR7","first-page":"19","volume-title":"Logic and Computer Science, volume 31 of APIC Series","author":"F Cardone","year":"1990","unstructured":"Cardone, F. and Coppo, M. (1990). Two extension of Curry2019s type inference system. In Odifreddi, P., editor, Logic and Computer Science, volume 31 of APIC Series, pages 19\u201375. Academic Press, New York, NY."},{"issue":"2","key":"42_CR8","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"PL Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T., and L\u00e9vy, J.-J. (1996). Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43 (2): 362\u2013397.","journal-title":"Journal of the Acm"},{"key":"42_CR9","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/351240.351259","volume-title":"Proceedings of the ACM Sigplan International Conference on Functional Programming (ICFP-00), volume 35.9 of ACM Sigplan Notices","author":"R Davies","year":"2000","unstructured":"Davies, R. and Pfenning, F. (2000). Intersection types and computational effects. In Proceedings of the ACM Sigplan International Conference on Functional Programming (ICFP-00), volume 35.9 of ACM Sigplan Notices, pages 198\u2013208, N.Y. ACM Press."},{"key":"42_CR10","unstructured":"Dezani-Ciancaglini, M., Honsell, F., and Motohama, Y. (2000). Compositional characterization of lambda -terms using intersection types. In Mathematical Foundation of Computer Science,volume 1893 of Lecture Notes in Computer Science,pages 304\u2013314. Springer-Verlag. extended abstract."},{"key":"42_CR11","first-page":"121","volume-title":"TLCA 2001-5th Int. Conf. on Typed Lambda Calculus and Applications, volume 2044 of Lecture Notes in Computer Science","author":"D Dougherty","year":"2001","unstructured":"Dougherty, D. and Lescanne, P. (2001). Reductions, intersection types, and explicit substitutions (extended abstract). In Abramsky, S., editor, TLCA 2001\u20135th Int. Conf. on Typed Lambda Calculus and Applications, volume 2044 of Lecture Notes in Computer Science, pages 121\u2013135, Krakow, Poland. Springer-Verlag."},{"key":"42_CR12","unstructured":"Dougherty, D. and Lescanne, P. (to appear). Reductions, intersection types, and explicit substitutions. Mathematical Structures in Computer Science."},{"issue":"1","key":"42_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jcss.2000.1703","volume":"62","author":"S Ghilezan","year":"2001","unstructured":"Ghilezan, S. (2001). Full intersection types and topologies in lambda calculus. JCSS: Journal of Computer and System Sciences, 62 (1): 1\u201314.","journal-title":"Jcss: Journal of Computer and System Sciences"},{"issue":"4","key":"42_CR14","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1017\/S0956796897002785","volume":"7","author":"F Kamareddine","year":"1997","unstructured":"Kamareddine, F. and R\u00edos, A. (1997). Extending a lambda-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. Journal of Functional Programming, 7 (4): 395\u2013420.","journal-title":"Journal of Functional Programming"},{"key":"42_CR15","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1145\/292540.292556","volume-title":"POPL \u201999. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 2022, 1999, San Antonio, TX, ACM SIGPLAN Notices","author":"AJ Kfoury","year":"1999","unstructured":"Kfoury, A. J. and Wells, J. B. (1999). Principality and decidable type inference for finite-rank intersection types. In ACM, editor, POPL \u201999. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 2022, 1999, San Antonio, TX, ACM SIGPLAN Notices, pages 161\u2013174, New York, NY, USA. ACM Press."},{"key":"42_CR16","unstructured":"Krivine, J.-L. (1993). Lambda calculus, types and models. Ellis Horwood."},{"key":"42_CR17","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/174675.174707","volume-title":"POPL \u201994-21st Annual ACM Symposium on Principles of Programming Languages","author":"P Lescanne","year":"1994","unstructured":"Lescanne, P. (1994). From\u03bb\u03c3 to \u03bb\u03c5: a journey through calculi of explicit substitutions. In Boehm, H.-J., editor, POPL \u201994\u201321st Annual ACM Symposium on Principles\n                    of Programming Languages, pages 60\u201369, Portland, Oregon. ACM."},{"key":"42_CR18","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"TLCA \u201995\u2014Int. Conf. on Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science","author":"PA Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.-A. (1995). Typed \u03bb-calculi with explicit substitution may not terminate. In Dezani, M., editor, TLCA \u201995\u2014Int. Conf. on Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 328\u2013334, Edinburgh, Scotland. Springer-Verlag."},{"key":"42_CR19","doi-asserted-by":"crossref","unstructured":"Ritter, E. (1999). Characterising explicit substitutions which preserve termination. In TLCA\u201999, Int. Conf. on Typed Lambda Calculus and Applications,volume 1581 of Lecture Notes in Computer Science,pages 325\u2013339. Springer-Verlag.","DOI":"10.1007\/3-540-48959-2_23"},{"key":"42_CR20","unstructured":"Rose, K. (1996). Operational Reduction Models for Functional Programming Languages. PhD thesis, DIKU, Universitetsparken 1, DK-2100 K\u00f8benhavn \u00d8. DIKU report 96\/1."},{"key":"42_CR21","unstructured":"van Bakel, S. and Dezani-Ciancaglini, M. (2002). Characterizing strong normalization for explicit substitutions. In Latin American Theoretical INformatics \u2014 LATIN. to appear."}],"container-title":["Foundations of Information Technology in the Era of Network and Mobile Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-35608-2_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T21:04:04Z","timestamp":1557781444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-35608-2_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9781475752755","9780387356082"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-35608-2_42","relation":{},"subject":[],"published":{"date-parts":[[2002]]}}}