{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:25:20Z","timestamp":1725488720393},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668367"},{"type":"electronic","value":"9783540466918"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46691-6_14","type":"book-chapter","created":{"date-parts":[[2007,8,9]],"date-time":"2007-08-09T20:42:24Z","timestamp":1186692144000},"page":"181-200","source":"Crossref","is-referenced-by-count":9,"title":["Explicit Substitutions and Programming Languages"],"prefix":"10.1007","author":[{"given":"Jean-Jacques","family":"L\u00e9vy","sequence":"first","affiliation":[]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,6,9]]},"reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1017\/S0956796800001696","volume":"6","author":"M. Abadi","year":"1996","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 6(2):pp. 299\u2013327, 1996. 181, 181","journal-title":"Journal of Functional Programming"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi, B. Lampson, and J.-J. L\u00e9vy. Analysis and caching of dependencies. In Proc. of the 1996 ACM SIGPLAN International Conference on Functional Programming, pages pp. 83\u201391. ACM Press, May 1996. 198, 198","DOI":"10.1145\/232629.232638"},{"key":"14_CR3","unstructured":"H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1981. 184, 192"},{"key":"14_CR4","unstructured":"Z.-E.-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. Lambda-upsilon, a calculus of explicit substitution which preserves strong normalisation. Research Report 2477, Inria, 1995. 181"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"G. Berry and J.-J. L\u00e9vy. Minimal and optima l computations of recursive programs. In Journal of the ACM, volume 26. ACM Press, 1979. 192","DOI":"10.1145\/322108.322122"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"B. Blanchet. Escape analysis: Correctness proof, implementation and experimental results. In Proc. of 25th ACM Symposium on Principles of Programming Languages. ACM Press, 1998. 196, 198","DOI":"10.1145\/268946.268949"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"R. Bloo and K. H. Rose. Combinatory reduction systems with explict substitutions thatpreserve strong normalization. In In Proc. of the 1996 confence on Rewriting Techniques and Applications. Springer, 1996. 181","DOI":"10.1007\/3-540-61464-8_51"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(97)00250-8","volume":"198","author":"N. \u00c7a\u011fman","year":"1998","unstructured":"N. \u00c7a\u011fman and J. R. Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198:pp. 239\u2013249, 1998. 182, 183","journal-title":"Theoretical Computer Science"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. In Proc. of the second international conference on Functional programming languages and computer architecture. ACM Press, 1985. 182","DOI":"10.1007\/3-540-15975-4_29"},{"key":"14_CR10","unstructured":"P.-L. Curien. Categorical Combinator, Sequential Algorithms and Functional Programming. Pitman, 1986. 181"},{"issue":"2","key":"14_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\u2019evy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):pp. 362\u2013397, 1996. 181","journal-title":"Journal of the ACM"},{"key":"14_CR12","unstructured":"R. David and B. Guillaume. The lambda I calculus. In Proc. of the Second International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 1999. 181"},{"key":"14_CR13","unstructured":"R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimitation in proof nets. In In Proc. of the 1997 symposium on Logics in Computer Science, 1997. 181"},{"key":"14_CR14","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, In proc. of the joint international conference and symphosium on Logic Programming, 1996. 182"},{"key":"14_CR15","first-page":"1","volume":"6","author":"J. Field","year":"1990","unstructured":"J. Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proc. of the Seventeenth conference on Principles of Programming Languages, volume 6, pages pp. 1\u201315. ACM Press, 1990. 181, 198","journal-title":"Proc. of the Seventeenth conference on Principles of Programming Languages"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"G. Gonthier, M. Abadi, and J.-J. L\u00e9vy. The geometry of optimal lambda reduction. In Proc. of the Nineteenth conference on Principles of Programming Languages, volume 8. ACM Press, 1992. 196","DOI":"10.1145\/143165.143172"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"T. Hardin. Confluence results for the pure strong categorical logic ccl. lambdacalculi as subsystems of ccl. Journal of Theoretical Computer Science, 65:291\u2013342, 1989. 181","journal-title":"Journal of Theoretical Computer Science"},{"issue":"2","key":"14_CR18","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1017\/S0956796898002986","volume":"8","author":"T. Hardin","year":"1998","unstructured":"T. Hardin, L. Maranget, and B. Pagano. Functional runtimes within the lambdasigma calculus. Journal of Functional Programming, 8(2), march 1998. 198","journal-title":"Journal of Functional Programming"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1002\/malq.19770230708","volume":"23","author":"J. R. Hindley","year":"1977","unstructured":"J. R. Hindley. Combinatory reductions and lambda reductions compared. Zeit. Math. Logik, 23:pp. 169\u2013180, 1977. 183","journal-title":"Zeit. Math. Logik"},{"key":"14_CR20","volume-title":"Combinatory Reduction Systems","author":"J.-W. Klop","year":"1980","unstructured":"J.-W. Klop. Combinatory Reduction Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980. 187"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"J. Launchbury. A natural semantics for lazy evaluation. In Proc. of the 1993 conference on Principles of Programming Languages. ACM Press, 1993. 194","DOI":"10.1145\/158511.158618"},{"key":"14_CR22","unstructured":"X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. 182, 196"},{"key":"14_CR23","unstructured":"P. Lescanne. From lambda-sigma to lambda-upsilon, a journey through calculi of explicit substitutions. In Proc. of the Twenty First conference on Principles of Programming Languages, 1994. 181"},{"key":"14_CR24","volume-title":"R\u00e9ductions correctes et optimales dans le lambda-calcul","author":"J.-J. L\u00e9vy","year":"1978","unstructured":"J.-J. L\u00e9vy. R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD thesis, Univ. of Paris 7, Paris, 1978. 192, 192"},{"key":"14_CR25","unstructured":"J.-J. L\u00e9vy. Optimal reductions in the lambda-calculus. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, 1980. On the occasion of his 80th birthday. 192, 192"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"L. Maranget. Optimal derivations in orthogonal term rewriting systems and in weak lambda calculi. In Proc. of the Eighteenth conference on Principles of Programming Languages. ACM Press, 1991. 192, 197","DOI":"10.1145\/99583.99618"},{"key":"14_CR27","volume-title":"La strat\u00e9gie paresseuse","author":"L. Maranget","year":"1992","unstructured":"L. Maranget. La strat\u00e9gie paresseuse. PhD thesis, Univ. of Paris 7, Paris, 1992. 192, 197"},{"key":"14_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Second conference on Typed Lambda-Calculi and Applications","author":"P.-A. Melli`es","year":"1995","unstructured":"P.-A. Melli`es. Typed lambda-calculus with explicit substitutions may not terminate. In Proc. of the Second conference on Typed Lambda-Calculi and Applications. Springer, 1995. LNCS 902. 181"},{"key":"14_CR29","unstructured":"P.-A. Melli`es. Description Abstraite des Syst`emes de R\u00e9\u00e9criture. PhD thesis, Univ. of Paris 7, december 1996. 187, 188, 197"},{"key":"14_CR30","unstructured":"R. Milner. Action calculi and the pi-calculus. In Proc. of the NATO Summer School on Logic and Computation. Marktoberdorf, 1993. 182"},{"key":"14_CR31","unstructured":"S. L. Peyton-Jones. The implementation of Functional Programming Languages. Prentice-Hall, 1987. 197"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46691-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T21:58:28Z","timestamp":1556747908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46691-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668367","9783540466918"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-46691-6_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}