{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:12:12Z","timestamp":1725516732399},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705826"},{"type":"electronic","value":"9783540705833"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_26","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"311-322","source":"Crossref","is-referenced-by-count":4,"title":["Perpetuality for Full and Safe Composition (in a Constructive Setting)"],"prefix":"10.1007","author":[{"given":"Delia","family":"Kesner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"26_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"4","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a04(1), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"26_CR2","unstructured":"Arbiser, A., Bonelli, E., R\u00edos, A.: Perpetuality in a lambda calculus with explicit substitutions and composition. WAIT, JAIIO (2000)"},{"issue":"1","key":"26_CR3","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1017\/S0960129500003248","volume":"11","author":"E. Bonelli","year":"2001","unstructured":"Bonelli, E.: Perpetuality in a named lambda calculus with explicit substitutions. Mathematical Structures in Computer Science\u00a011(1), 47\u201390 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1017\/S0960129500003224","volume":"11","author":"R. David","year":"2001","unstructured":"David, R., Guillaume, B.: A \u03bb-calculus with explicit weakening and explicit substitution. Mathematical Structures in Computer Science\u00a011, 169\u2013206 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"26_CR5","unstructured":"de Bruijn, N.G.: Generalizing Automath by Means of a Lambda-Typed Lambda Calculus. In: Mathematical Logic and Theoretical Computer Science. Lecture Notes in Pure and Applied Mathematics, vol.\u00a0106 (1987)"},{"issue":"3","key":"26_CR6","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1017\/S0960129502003791","volume":"13","author":"R. Cosmo Di","year":"2003","unstructured":"Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. Mathematical Structures in Computer Science\u00a013(3), 409\u2013450 (2003)","journal-title":"Mathematical Structures in Computer Science"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. Information and Computation\u00a0157, 183\u2013235 (2000)","journal-title":"Information and Computation"},{"key":"26_CR8","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieure. Th\u00e8se de doctorat d\u2019\u00e9tat, Univ. Paris VII (1972)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"26_CR10","unstructured":"Hardin, T., L\u00e9vy, J.-J.: A confluent calculus of substitutions. In: France-Japan Artificial Intelligence and Computer Science Symposium, Izu, Japan (1989)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-540-74915-8_20","volume-title":"Computer Science Logic","author":"D. Kesner","year":"2007","unstructured":"Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 238\u2013252. Springer, Heidelberg (2007)"},{"key":"26_CR12","unstructured":"Kesner, D.: Perpetuality for full and safe composition (in a constructive setting) (2008), http:\/\/www.pps.jussieu.fr\/~kesner\/papers\/"},{"key":"26_CR13","unstructured":"Kesner, D., \u00d3 Conch\u00fair, S.: Fundamental properties of Milner\u2019s non-local explicit substitution calculus, http:\/\/www.pps.jussieu.fr\/~kesner\/papers\/"},{"issue":"4","key":"26_CR14","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/j.ic.2006.08.008","volume":"205","author":"D. Kesner","year":"2007","unstructured":"Kesner, D., Lengrand, S.: Resource operators for lambda-calculus. Information and Computation\u00a0205(4), 419\u2013473 (2007)","journal-title":"Information and Computation"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/3-540-45127-7_11","volume-title":"Rewriting Techniques and Applications","author":"Z. Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Uniform Normalisation beyond Orthogonality. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 122\u2013136. Springer, Heidelberg (2001)"},{"key":"26_CR16","unstructured":"Klop, J.-W.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127. CWI, Amsterdam (1980)"},{"key":"26_CR17","unstructured":"Lengrand, S.: Normalisation and Equivalence in Proof Theory and Type Theory. PhD thesis, University Paris 7 and University of St Andrews (November 2006)"},{"issue":"1","key":"26_CR18","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.ic.2003.09.004","volume":"189","author":"S. Lengrand","year":"2004","unstructured":"Lengrand, S., Lescanne, P., Dougherty, D., Dezani-Ciancaglini, M., van Bakel, S.: Intersection types for explicit substitutions. Information and Computation\u00a0189(1), 17\u201342 (2004)","journal-title":"Information and Computation"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-46691-6_14","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"J.-J. L\u00e9vy","year":"1999","unstructured":"L\u00e9vy, J.-J., Maranget, L.: Explicit substitutions and programming languages. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 181\u2013200. Springer, Heidelberg (1999)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-16780-3_82","volume-title":"8th International Conference on Automated Deduction","author":"R. Lins","year":"1986","unstructured":"Lins, R.: A new formula for the execution of categorical combinators. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 89\u201398. Springer, Heidelberg (1986)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"TLCA","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.-A.: Typed \u03bb-calculi with explicit substitutions may not terminate. In: TLCA. LNCS, vol.\u00a0902, pp. 328\u2013334. Springer, Heidelberg (1995)"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Milner, R.: Local bigraphs and confluence: two conjectures. In: EXPRESS. ENTCS vol. 175 (2006)","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-58150-2","volume-title":"CTRS","author":"K. Rose","year":"1992","unstructured":"Rose, K.: Explicit cyclic substitutions. In: CTRS. LNCS, vol.\u00a0656. Springer, Heidelberg (1992)"},{"key":"26_CR24","unstructured":"Sakurai, T.: Strong normalizability of calculus of explicit substitutions with composition, http:\/\/www.math.s.chiba-u.ac.jp\/~sakurai\/papers.html"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-44881-0_5","volume-title":"Rewriting Techniques and Applications","author":"F.-R. Sinot","year":"2003","unstructured":"Sinot, F.-R., Fern\u00e1ndez, M., Mackie, I.: Efficient reductions with director strings. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 46\u201360. Springer, Heidelberg (2003)"},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Tait, W.: Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic\u00a032 (1967)","DOI":"10.2307\/2271658"},{"key":"26_CR27","unstructured":"van Daalen, D.T.: The language theory of automath. PhD thesis, Technische Hogeschool Eindhoven (1977)"},{"key":"26_CR28","unstructured":"van Raamsdonk, F.: Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Amsterdam University, Netherlands (1996)"},{"key":"26_CR29","unstructured":"Sinot, F.-R., van Oostrom, V.: Preserving termination of the \u0142-calculus or not (unpublished note) (2007)"},{"key":"26_CR30","doi-asserted-by":"crossref","unstructured":"van Raamsdonk, F., Severi, P., Sorensen, M.H., Xi, H.: Perpetual reductions in \u03bb-calculus. Information and Computation\u00a0149(2) (1999)","DOI":"10.1006\/inco.1998.2750"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:07:58Z","timestamp":1605744478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}