{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214709},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540419600"},{"type":"electronic","value":"9783540454137"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45413-6_13","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T08:51:43Z","timestamp":1186217503000},"page":"121-135","source":"Crossref","is-referenced-by-count":5,"title":["Reductions, intersection types, and explicit substitutions"],"prefix":"10.1007","author":[{"given":"Dan","family":"Doughertyy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Lescanne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,4,25]]},"reference":[{"issue":"4","key":"13_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":"13_CR2","volume-title":"Studies in Logic and the Foundation of Mathematics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier, Amsterdam, 1984. Second edition.","edition":"Second edition"},{"key":"13_CR3","unstructured":"H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabby, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117\u2013309. Oxford University Press, 1992."},{"issue":"5","key":"13_CR4","doi-asserted-by":"crossref","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. \u03bb\u03bd, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6(5):699\u2013722, September 1996.","journal-title":"Journal of Functional Programming"},{"key":"13_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1007\/3-540-61756-6_99","volume-title":"PLILP\u2019 96\u20148th Int. Symp. on Programming Languages: Implementation, Logics and Programs","author":"Z. Benaissa","year":"1996","unstructured":"Z. Benaissa, P. Lescanne, and K. H. Rose. Modeling sharing and recursion for weak reduction strategies using explicit substitution. In H. Kuchen and D. Swierstra, editors, PLILP\u2019 96\u20148th Int. Symp. on Programming Languages: Implementation, Logics and Programs, number 1140 in LNCS, pages 393\u2013407, Aachen, Germany, September 1996. Springer-Verlag."},{"key":"13_CR6","unstructured":"R. Bloo. Preservation of Termination for Explicit Substitution. PhD thesis, Technische Universiteit Eindhoven, 1997. IPA Dissertation Series 1997-05."},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"R. Bloo","year":"1999","unstructured":"R. Bloo and J. H. Geuvers. Explicit substitution: on the edge of strong normalization. Theoretical Computer Science, 211:375\u2013395, 1999.","journal-title":"Theoretical Computer Science"},{"key":"13_CR8","unstructured":"R. Bloo and K. H. Rose. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In CSN\u2019 95\u2014Computing Science in the Netherlands, pages 62\u201372, Utrecht, November 1995."},{"key":"13_CR9","unstructured":"E. Bonelli. Perpetuality in a named lambda calculus with explicit substitutions and some applications. Technical Report RR 1221, LRI, University of Paris-Sud, 1999. to appear in MSCS, 2000."},{"key":"13_CR10","series-title":"APIC Series","first-page":"19","volume-title":"Logic and Computer Science","author":"F. Cardone","year":"1990","unstructured":"F. Cardone and M. Coppo. Two extension of Curry\u2019s type inference system. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Series, pages 19\u201375. Academic Press, New York, NY, 1990."},{"issue":"2","key":"13_CR11","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362\u2013397, March 1996.","journal-title":"Journal of the ACM"},{"key":"13_CR12","volume-title":"Combinatory Logic I","author":"H. B. Curry","year":"1958","unstructured":"H. B Curry and R. Feys. Combinatory Logic I. North-Holland, Amsterdam, 1958."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets. In LICS\u2019 97\u2014Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 35\u201346. Warsaw U., IEEE, June 1997.","DOI":"10.1109\/LICS.1997.614927"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. Relating the lambda-sigma and lambda-s styles of explicit substitutions. Journal of Logic and Computation, 10(3), 2000. Special issue on Type Theory and Term Rewriting.","DOI":"10.1093\/logcom\/10.3.349"},{"issue":"3","key":"13_CR15","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1142\/S0129054193000146","volume":"4","author":"F. Kamereddine","year":"1993","unstructured":"F. Kamereddine and R.P. Nederpelt. On stepwise explicit substitutions. International Journal of Foundations of Computer Science, 4(3):197\u2013240, 1993.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From \u03bb\u03c3 to \u03bb\u03bd: a journey through calculi of explicit substitutions. In Hans-J. Boehm, editor, POPL\u2019 94\u201421st Annual ACM Symposium on Principles of Programming Languages, pages 60\u201369, Portland, Oregon, January 1994. ACM.","DOI":"10.1145\/174675.174707"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"TLCA\u2019 95\u2014Int. Conf. on Typed Lambda Calculus and Applications","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitution may not terminate. In M. Dezani, editor, TLCA\u2019 95\u2014Int. Conf. on Typed Lambda Calculus and Applications, volume 902 of LNCS, pages 328\u2013334, Edinburgh, Scotland, April 1995. Springer-Verlag."},{"key":"13_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0026981","volume-title":"Proceedings of the 7th Conference on Category Theory and Computer Science","author":"P.-A. Melli\u00e9s","year":"1997","unstructured":"P.-A. Melli\u00e9s. Axiomatic rewriting theory III, a factorisation theorem in rewriting theory. In Proceedings of the 7th Conference on Category Theory and Computer Science, volume 1290 of LNCS, pages 49\u201368. Springer-Verlag, 1997."},{"key":"13_CR19","volume-title":"Foundations for Programming Languages","author":"J. C. Mitchell","year":"1996","unstructured":"J. C. Mitchell. Foundations for Programming Languages. MIT Press, Cambridge, MA, 1996."},{"key":"13_CR20","series-title":"Lect Notes Comput Sci","volume-title":"TLCA\u201999","author":"E. Ritter","year":"1999","unstructured":"E. Ritter. Characterising explicit substitutions which preserve termination. In TLCA\u201999, volume 1581 of LNCS. Springer-Verlag, 1999."},{"key":"13_CR21","unstructured":"K.H. Rose. Operational Reduction Models for Functional Programming Languages. PhD thesis, DIKU, Kobenhavn, February 1996. DIKU report 96\/1."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45413-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:06:53Z","timestamp":1556737613000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45413-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540419600","9783540454137"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45413-6_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}