{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:08Z","timestamp":1725566648973},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_30","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"407-422","source":"Crossref","is-referenced-by-count":8,"title":["Extending the Explicit Substitution Paradigm"],"prefix":"10.1007","author":[{"given":"Delia","family":"Kesner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"30_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. JFP\u00a04(1), 375\u2013416 (1991)","journal-title":"JFP"},{"key":"30_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S.: Computational interpretations of linear logic. TCS\u00a0111, 3\u201357 (1993)","journal-title":"TCS"},{"key":"30_CR3","unstructured":"Arbiser, A., Bonelli, E., R\u00edos, A.: Perpetuality in a lambda calculus with explicit substitutions and composition. WAIT, JAIIO (2000)"},{"key":"30_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"The Optimal Implementation of Functional Programming Languages","author":"A. Asperti","year":"1998","unstructured":"Asperti, A., Guerrini, S.: The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, vol.\u00a045. Cambridge University Press, Cambridge (1998)"},{"issue":"5","key":"30_CR5","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z.-E.-A. Benaissa","year":"1996","unstructured":"Benaissa, Z.-E.-A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: \u03bb\u03c5, a calculus of explicit substitutions which preserves strong normalisation. JFP\u00a06(5), 699\u2013722 (1996)","journal-title":"JFP"},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"Typed Lambda Calculi and Applications","author":"N. Benton","year":"1993","unstructured":"Benton, N., Bierman, G., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 75\u201390. Springer, Heidelberg (1993)"},{"issue":"1-2","key":"30_CR7","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1016\/S0304-3975(97)00183-7","volume":"211","author":"R. Bloo","year":"1999","unstructured":"Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalization. TCS\u00a0211(1-2), 375\u2013395 (1999)","journal-title":"TCS"},{"key":"30_CR8","unstructured":"Bloo, R., Rose, K.: Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection. In: Computing Science in the Netherlands, Netherlands Computer Science Research Foundation, pp. 62\u201372 (1995)"},{"issue":"1","key":"30_CR9","first-page":"409","volume":"11","author":"E. Bonelli","year":"2001","unstructured":"Bonelli, E.: Perpetuality in a named lambda calculus with explicit substitutions. MSCS\u00a011(1), 409\u2013450 (2001)","journal-title":"MSCS"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Cerrito, S., Kesner, D.: Pattern matching as cut elimination. In: LICS, pp. 98\u2013108 (1999)","DOI":"10.1109\/LICS.1999.782596"},{"key":"30_CR11","volume-title":"The calculi of lambda conversion","author":"A. Church","year":"1941","unstructured":"Church, A.: The calculi of lambda conversion. Princeton University Press, Princeton (1941)"},{"key":"30_CR12","unstructured":"The Coq Proof Assistant, http:\/\/coq.inria.fr\/"},{"key":"30_CR13","volume-title":"Advances in Linear Logic","author":"V. Danos","year":"1995","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: Sequent calculi for second order logic. In: Advances in Linear Logic, Cambridge University Press, Cambridge (1995)"},{"key":"30_CR14","first-page":"169","volume":"11","author":"R. David","year":"2001","unstructured":"David, R., Guillaume, B.: A \u03bb-calculus with explicit weakening and explicit substitution. MSCS\u00a011, 169\u2013206 (2001)","journal-title":"MSCS"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-48685-2_6","volume-title":"Rewriting Techniques and Applications","author":"R. Cosmo Di","year":"1999","unstructured":"Di Cosmo, R., Guerrini, S.: Strong normalization of proof nets modulo structural congruences. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 75\u201389. Springer, Heidelberg (1999)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Di Cosmo, R., Kesner, D.: Strong normalization of explicit substitutions via cut elimination in proof nets. In: LICS, pp. 35\u201346 (1997)","DOI":"10.1109\/LICS.1997.614927"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-46432-8_5","volume-title":"Foundation of Software Science and Computation Structures","author":"R. Cosmo Di","year":"2000","unstructured":"Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol.\u00a01784, pp. 63\u201381. Springer, Heidelberg (2000)"},{"issue":"3","key":"30_CR18","first-page":"409","volume":"13","author":"R. Cosmo Di","year":"2003","unstructured":"Di Cosmo, R., Kesner, D., Polonovski, E.: Proof nets and explicit substitutions. MSCS\u00a013(3), 409\u2013450 (2003)","journal-title":"MSCS"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-45413-6_13","volume-title":"Typed Lambda Calculi and Applications","author":"D. Dougherty","year":"2001","unstructured":"Dougherty, D., Lescanne, P.: Reductions, Intersection Types and Explicit Substitutions. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 121\u2013135. Springer, Heidelberg (2001)"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: LICS (1995)","DOI":"10.1109\/LICS.1995.523271"},{"key":"30_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-48168-0_16","volume-title":"Computer Science Logic","author":"M. Fern\u00e1ndez","year":"1999","unstructured":"Fern\u00e1ndez, M., Mackie, I.: Closed reductions in the lambda calculus. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 220\u2013234. Springer, Heidelberg (1999)"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45610-4_13","volume-title":"Rewriting Techniques and Applications","author":"J. Forest","year":"2002","unstructured":"Forest, J.: A weak calculus with explicit operators for pattern matching and substitution. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 174\u2013191. Springer, Heidelberg (2002)"},{"issue":"1","key":"30_CR23","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1093\/jigpal\/8.1.7","volume":"8","author":"N. Ghani","year":"2000","unstructured":"Ghani, N., de Paiva, V., Ritter, E.: Linear explicit substitutions. IGPL\u00a08(1), 7\u201331 (2000)","journal-title":"IGPL"},{"issue":"1","key":"30_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. TCS\u00a050(1), 1\u2013101 (1987)","journal-title":"TCS"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/BFb0097790","volume-title":"Types for Proofs and Programs","author":"J. Goubault-Larrecq","year":"1998","unstructured":"Goubault-Larrecq, J.: A proof of weak termination of typed lambda sigma-calculi. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 134\u2013151. Springer, Heidelberg (1998)"},{"key":"30_CR26","unstructured":"Hardin, T.: R\u00e9sultats de confluence pour les r\u00e8gles fortes de la logique combinatoire cat\u00e9gorique et liens avec les lambda-calculs. PhD Thesis, Universit\u00e9 Paris 7 (1987)"},{"key":"30_CR27","unstructured":"Hardin, T., L\u00e9vy, J.-J.: A confluent calculus of substitutions. In: France-Japan Artificial Intelligence and Computer Science Symposium (1989)"},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambdasigma calculus. In: ICFP (1996)","DOI":"10.1145\/232627.232632"},{"key":"30_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-45085-6_11","volume-title":"Automated Deduction \u2013 CADE-19","author":"D. Hendriks","year":"2003","unstructured":"Hendriks, D., van Oostrom, V.: reflectbox{ lambda}. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 136\u2013150. Springer, Heidelberg (2003)"},{"key":"30_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H. Herbelin","year":"1995","unstructured":"Herbelin, H.: A l-calculus structure isomorphic to sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, Springer, Heidelberg (1995)"},{"key":"30_CR31","unstructured":"The HOL system, http:\/\/www.dcs.gla.ac.uk\/~tfm\/fmt\/hol.html"},{"key":"30_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0026813","volume-title":"Programming Languages: Implementations, Logics and Programs","author":"F. Kamareddine","year":"1995","unstructured":"Kamareddine, F., R\u00edos, A.: A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol.\u00a0982, pp. 45\u201362. Springer, Heidelberg (1995)"},{"key":"30_CR33","unstructured":"Kesner, D., Lengrand, S.: An Explicit Operator Calculus as the Syntactic Counterpart to a Proof-Net Model (2004), Available at http:\/\/www.pps.jussieu.fr\/~kesner\/papers"},{"key":"30_CR34","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 Normalization Beyond Orthogonality. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 122\u2013136. Springer, Heidelberg (2001)"},{"key":"30_CR35","series-title":"Mathematical Centre Tracts","volume-title":"Combinatory Reduction Systems, PhD Thesis","author":"J.-W. Klop","year":"1980","unstructured":"Klop, J.-W.: Combinatory Reduction Systems, PhD Thesis. Mathematical Centre Tracts, vol.\u00a0127. CWI, Amsterdam (1980)"},{"key":"30_CR36","doi-asserted-by":"crossref","unstructured":"Lafont, Y.: Interaction Nets. POPL, pp. 95\u2013108 (1990)","DOI":"10.1145\/96709.96718"},{"issue":"290","key":"30_CR37","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0304-3975(01)00297-3","volume":"1","author":"O. Laurent","year":"2003","unstructured":"Laurent, O.: Polarized proof-nets and lambda-mu calculus. TCS\u00a01(290), 161\u2013188 (2003)","journal-title":"TCS"},{"issue":"1","key":"30_CR38","first-page":"17","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. I & C\u00a0189(1), 17\u201342 (2004)","journal-title":"I & C"},{"key":"30_CR39","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., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 181\u2013200. Springer, Heidelberg (1999)"},{"key":"30_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0014062","volume-title":"Typed Lambda Calculi and Applications","author":"P.-A. Melli\u00e8s","year":"1995","unstructured":"Melli\u00e8s, P.-A.: Typed \u03bb-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 328\u2013334. Springer, Heidelberg (1995)"},{"key":"30_CR41","unstructured":"Nederpelt, R.: Strong Normalization in a Typed Lambda Calculus with Lambda Structured Types. PhD Thesis, Eindhoven University of Technology (1973)"},{"key":"30_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"30_CR43","unstructured":"Polonovski, E.: Substitutions explicites et preuves de normalisation. PhD thesis, Universit\u00e9 Paris 7 (2004)"},{"issue":"126","key":"30_CR44","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"2","author":"L. Regnier","year":"1994","unstructured":"Regnier, L.: Une \u00e9quivalence sur les lambda-termes. TCS\u00a02(126), 281\u2013292 (1994)","journal-title":"TCS"},{"key":"30_CR45","doi-asserted-by":"crossref","unstructured":"Ronchi della Rocca, S., Roversi, L.: Lambda calculus and intuitionistic linear logic. Studia Logica\u00a059(3) (1997)","DOI":"10.1023\/A:1005092630115"},{"key":"30_CR46","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":"30_CR47","first-page":"35","volume":"37","author":"M.H. Sorensen","year":"1997","unstructured":"Sorensen, M.H.: Strong Normalization From Weak Normalization in Typed Lambda-Calculi. I&C\u00a037, 35\u201371 (1997)","journal-title":"I&C"},{"key":"30_CR48","unstructured":"van Oostrom, V.: Net-calculus (2001), Course Notes available on http:\/\/www.phil.uu.nl\/~oostrom\/typcomp\/00-01\/net.ps"},{"key":"30_CR49","doi-asserted-by":"crossref","unstructured":"Vestergaard, R., Wells, J.: Cut Rules and Explicit Substitutions. MSCS\u00a011(1) (2001)","DOI":"10.1017\/S0960129500003273"},{"key":"30_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/3-540-58027-1_24","volume-title":"Mathematical Foundations of Programming Semantics","author":"P. Wadler","year":"1994","unstructured":"Wadler, P.: A syntax for linear logic. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol.\u00a0802, pp. 513\u2013529. Springer, Heidelberg (1994)"},{"key":"30_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-62688-3_48","volume-title":"Typed Lambda Calculi and Applications","author":"H. Xi","year":"1997","unstructured":"Xi, H.: Weak and Strong Beta Normalisations in Typed Lambda-Calculi. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol.\u00a01210, pp. 390\u2013404. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:34:00Z","timestamp":1605760440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}