{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T22:24:53Z","timestamp":1648679093695},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2005,2,22]],"date-time":"2005-02-22T00:00:00Z","timestamp":1109030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s00200-005-0169-9","type":"journal-article","created":{"date-parts":[[2005,2,22]],"date-time":"2005-02-22T05:57:29Z","timestamp":1109051849000},"page":"393-437","source":"Crossref","is-referenced-by-count":6,"title":["Lambda-Calculus with Director Strings"],"prefix":"10.1007","volume":"15","author":[{"given":"Maribel","family":"Fern\ufffdndez","sequence":"first","affiliation":[]},{"given":"Ian","family":"Mackie","sequence":"additional","affiliation":[]},{"given":"Fran\ufffdois-R\ufffdgis","family":"Sinot","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,22]]},"reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"Abadi","year":"4","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. J. Funct. Prog. 1(4), 375?416 (1991)","journal-title":"J. Funct. Prog."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (POPL?95), ACM Press, 1995, pp. 233?246","DOI":"10.1145\/199448.199507"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"763","DOI":"10.1017\/S0956796800001994","volume":"6","author":"Asperti","year":"6","unstructured":"Asperti, A., Giovanetti, C., Naletto, A.: The Bologna optimal higher-order machine. J. Funct. Prog. 6(6), 763?810 (1996)","journal-title":"J. Funct. Prog."},{"key":"CR4","unstructured":"Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998"},{"key":"CR5","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984"},{"key":"CR6","unstructured":"Barendregt, H.P.: Lambda calculi with types. In: Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, T.S.E. Maibaum, (eds.), Oxford University Press, 1992"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Benaissa","year":"5","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli., J.: Lambda-upsilon, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming 6(5), 699?722 (1996)","journal-title":"Journal of Functional Programming"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Benaissa, Z., Rose, K.H., Lescanne, P.: Modeling sharing and recursion for weak reduction strategies using explicit substitution. In: 8th PLILP?-Symposium on Programming Language Implementation and Logic Programming, H. Kuchen, D. Swierstra, (eds.), Aachen, Germany, 1996, pp. 393?407","DOI":"10.1007\/3-540-61756-6_99"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"Bloo","year":"1","unstructured":"Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalization. Theor. Comp. Sci. 211(1), 375?395 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Cr\u00e9gut, P.: An abstract machine for lambda-terms normalization. In: Lisp and Functional Programming 1990, ACM Press, 1990, pp. 333?340","DOI":"10.1145\/91556.91681"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"Curien","year":"2","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362?397 (1996)","journal-title":"Journal of the ACM"},{"key":"CR12","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1017\/S0960129500003224","volume":"11","author":"David","year":"1","unstructured":"David, R., Guillaume, B.: A ?-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science 11(1), 169?206 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies. Indagationes Mathematicae, 34, 381?392 (1972)","journal-title":"Indagationes Mathematicae,"},{"key":"CR14","unstructured":"de Bruijn, N.G.: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report T.H.-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology, 1978"},{"key":"CR15","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science: Formal Methods and Semantics, J. van Leeuwen, (ed.), volume B. North-Holland, 1989"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Ennals, R., Jones, S.P.: Optimistic evaluation: an adaptive evaluation strategy for non-strict programs. In: Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP-03), C. Norris, J. James, B. Fenwick (eds.), volume 38, 9 of ACM SIGPLAN Notices, ACM Press, 2003, pp. 287?298","DOI":"10.1145\/944705.944731"},{"key":"CR17","unstructured":"Fern\u00e1ndez, M., Mackie, I.: Closed reductions in the ?-calculus. In: Proceedings of Computer Science Logic (CSL?99), J. Flum, M. Rodr\u00edguez-Artalejo (eds.), number 1683 in Lecture Notes in Computer Sciences, Springer-Verlag, 1999, pp. 220?234"},{"key":"CR18","unstructured":"Fern\u00e1ndez, M., Mackie, I.: Director strings and explicit substitutions. WESTAPP?01, Utrecht, 2001"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Abadi, M., L\u00e9vy, J.-J.: The geometry of optimal lambda reduction. In: Proceedings of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albequerque, New Mexico, 1992, pp. 15?26","DOI":"10.1145\/143165.143172"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of ICFP?02, Pittsburgh, Pennsylvania, USA, 2002","DOI":"10.1145\/581478.581501"},{"key":"CR21","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/S0956796898002986","volume":"8","author":"Hardin","year":"2","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional runtime systems within the lambda-sigma calculus. J. Funct. Prog. 8(2), 131?176 (1998)","journal-title":"J. Funct. Prog."},{"key":"CR22","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1145\/48022.48026","volume":"10","author":"Kennaway","year":"4","unstructured":"Kennaway, J., Sleep, M.: Director strings as combinators. ACM Transactions on Programming Languages and Systems 10(4), 602?626 (1988)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Lamping, J.: An algorithm for optimal lambda calculus reductions. In: Proceedings 17 th ACM Symposium on Principles of Programming Languages, 1990, pp. 16?30","DOI":"10.1145\/96709.96711"},{"key":"CR24","unstructured":"Lang, F.: Mod\u00e8les de la ?-r\u00e9duction pour les implantations. PhD thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon, 1998"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Lawall, J.L., Mairson, H.G.: Optimality and inefficiency: What isn?t a cost model of the lambda calculus? In: International Conference on Functional Programming, 1996, pp. 92?101","DOI":"10.1145\/232627.232639"},{"key":"CR26","unstructured":"Lescanne, P.: From ?? to ??: a journey through calculi of explicit substitutions. In: Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL?94). ACM Press, 1994"},{"key":"CR27","unstructured":"Lescanne, P., Rouyer-Degli, J.: The calculus of explicit substitutions lambda-upsilon. Technical Report RR-2222, INRIA, 1995"},{"key":"CR28","unstructured":"L\u00e9vy, J.-J.: Optimal reductions in the lambda-calculus. In: To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin, J.R. Hindley (eds.), Academic Press, 1980, pp. 159?191"},{"key":"CR29","unstructured":"Melli\u00e8s, P.-A.: Typed lambda-calculi with explicit substitutions may not terminate. In: Proceedings of the 2nd International Conference on Typed Lambda Calculi and Applications, number 902 in Lecture Notes in Computer Science, Springer-Verlag, 1995, pp. 328?334"},{"key":"CR30","first-page":"1999","volume":"1999","author":"Nadathur","year":"2","unstructured":"Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), 1999","journal-title":"Journal of Functional and Logic Programming,"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Nadathur, G.: The suspension notation for lambda terms and its use in metalanguage implementations. In: Electronic Notes in Theoretical Computer Science, R. de Queiroz, L.C. Pereira, E.H. Haeusler (eds.), volume 67. Elsevier, 2002","DOI":"10.1016\/S1571-0661(04)80539-5"},{"key":"CR32","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"Newman","year":"2","unstructured":"Newman, M.: On theories with a combinatorial definition of ??equivalence??. Annals of Mathematics 43(2), 223?243 (1942)","journal-title":"Annals of Mathematics"},{"key":"CR33","unstructured":"Rose, K.: Explicit substitution - tutorial and survey, 1996. Lecture Series LS-96-3, BRICS, Dept. of Computer Science, University of Aarhus, Denmark"},{"key":"CR34","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"Rosen","year":"1","unstructured":"Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM 20(1), 160?187 (1973)","journal-title":"Journal of the ACM"},{"key":"CR35","unstructured":"Sinot, F.-R., Fern\u00e1ndez, M., Mackie, I.: Efficient reductions with director strings. In: Proceedings of Rewriting Techniques and Applications (RTA?03), R. Nieuwenhuis (ed), volume 2706 of Lecture Notes in Computer Science, Springer-Verlag, 2003, pp. 46?60"},{"key":"CR36","first-page":"3","volume":"11","author":"Yoshida","year":"6","unstructured":"Yoshida, N.: Optimal reduction in weak lambda-calculus with shared environments. Journal of Computer Software, 11(6), 3?18 (1994)","journal-title":"Journal of Computer Software,"}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0169-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00200-005-0169-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-005-0169-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T11:24:18Z","timestamp":1558610658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00200-005-0169-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2,22]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["169"],"URL":"https:\/\/doi.org\/10.1007\/s00200-005-0169-9","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2,22]]}}}