{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:40:54Z","timestamp":1725496854611},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_16","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"220-234","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Closed Reductions in the \u03bb-Calculus"],"prefix":"10.1007","author":[{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"first","affiliation":[]},{"given":"Ian","family":"Mackie","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"issue":"4","key":"16_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":"16_CR2","doi-asserted-by":"crossref","unstructured":"Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL\u201995), pages 233\u2013246. ACM Press, 1995.","DOI":"10.1145\/199448.199507"},{"issue":"2","key":"16_CR3","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, 1996.","journal-title":"Journal of the ACM"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"J.-Y. Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, eds, Logic Colloquium 88, Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company, 1989.","DOI":"10.1016\/S0049-237X(08)70271-4"},{"issue":"2","key":"16_CR5","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796898002986","volume":"8","author":"T. Hardin","year":"1998","unstructured":"T. Hardin, L. Maranget, and B. Pagano. Functional back-ends within the lambdasigma calculus. Journal of Functional Programming, 8(2):131\u2013172, 1998.","journal-title":"Journal of Functional Programming"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1145\/48022.48026","volume":"10","author":"J. Kennaway","year":"1988","unstructured":"J. Kennaway and M. Sleep. Director strings as combinators. ACM Transactions on Programming Languages and Systems, 10:602\u2013626, 1988.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR7","unstructured":"P. Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions lambdaupsilon. Technical Report RR-2222, INRIA, 1995."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"I. Mackie. YALE: Yet another lambda evaluator based on interaction nets. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP\u201998), pages 117\u2013128. ACM Press, 1998.","DOI":"10.1145\/289423.289434"},{"key":"16_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Proceedings of the Second International Conference on Typed Lambda Calculi and Applications","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"P.-A. Melli\u00e8s. Typed lambda-calculi with explicit substitutions may not terminate. In Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, number 902 in Lecture Notes in Computer Science, pages 328\u2013334. Springer-Verlag, 1995."},{"key":"16_CR10","volume-title":"Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science","author":"C. Mu\u00f1oz","year":"1996","unstructured":"C. Mu\u00f1oz. Confluence and preservation of strong normalisation in an explicit substitutions calculus (extended abstract). In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey. IEEE Computer Society Press, 1996."},{"issue":"3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G. Plotkin","year":"1977","unstructured":"G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223\u2013256, 1977.","journal-title":"Theoretical Computer Science"},{"key":"16_CR12","volume-title":"Lecture Series LS-96-3","author":"K. H. Rose","year":"1996","unstructured":"K. H. Rose. Explicit substitution-tutorial and survey. Lecture Series LS-96-3, BRICS, Dept. of Computer Science, University of Aarhus, Denmark, 1996."},{"issue":"6","key":"16_CR13","first-page":"3","volume":"11","author":"N. Yoshida","year":"1994","unstructured":"N. Yoshida. Optimal reduction in weak lambda-calculus with shared environments. Journal of Computer Software, 11(6):3\u201318, 1994.","journal-title":"Journal of Computer Software"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T04:08:41Z","timestamp":1586146121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}