{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:04:54Z","timestamp":1743102294176,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008972"},{"type":"electronic","value":"9783540365761"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36576-1_10","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"153-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Normalisation Result for Higher-Order Calculi with Explicit Substitutions"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"4","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P-L. Curien,and J-J. L\u00e9vy.Explicit substitutions. Journal of Functional Programming 4(1):375\u201316,1991.","journal-title":"Journal of Functional Programming"},{"key":"10_CR2","unstructured":"H.P. Barendregt.The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103.North-Holland, Amsterdam,revised edition,1984."},{"issue":"5","key":"10_CR3","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne,and J. Rouyer-Degli.\u03bb\u03bd,a calculus of explicit substitutions which preserves strong normalisation.Journal of Functional Programming 6(5):699\u201322,1996.","journal-title":"Journal of Functional Programming"},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","volume-title":"A de Bruijn notation for Higher-Order Rewriting","author":"E. Bonelli","year":"2000","unstructured":"E. Bonelli, D. Kesner,and A. R\u00edos.A de Bruijn notation for Higher-Order Rewriting.In Proceedings of the 11th RTA number 1833 in LNCS. Springer-Verlag,2000."},{"key":"10_CR5","series-title":"Lect Notes Comput Sci","volume-title":"From Higher-Order to First-Order Rewriting","author":"E. Bonelli","year":"2001","unstructured":"E. Bonelli, D. Kesner,and A.R\u00edos.From Higher-Order to First-Order Rewriting.In Proceedings of the 12th RTA number 2051 in LNCS. Springer-Verlag,2001."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term Rewriting and All That. Cambridge University Press,1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"10_CR7","unstructured":"E. Bonelli.Term rewriting and explicit substitutions. PhD thesis,Universit\u00e9 de Paris Sud,November 2001."},{"key":"10_CR8","unstructured":"E. Bonelli.A normalisation result for higher-order calculi with explicit substitutions,2003.Full version of this paper. http:\/\/www-lifia.info.unlp.edu.ar\/~eduardo\/."},{"key":"10_CR9","unstructured":"G. Boudol.Computational semantics of term rewrite systems.In M. Nivat and J.C. Reynolds,editors,Algebraic methods in Semantics Cambridge University Press,1985."},{"key":"10_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-55808-X_19","volume-title":"Strong normalization of substitutions","author":"P.-L. Curien","year":"1992","unstructured":"P-L. Curien, T. Hardin,and A. R\u00edos.Strong normalization of substitutions.In Proceedings of Mathematical Foundations of Computer Science, number 629 in LNCS,pages 209\u201317.Springer-Verlag,1992."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn.Lambda calculus notation with nameless dummies,a tool for automatic formula manipulation with application to the church-rosser theorem.Indag. Mat., 5(35),1972.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"R. David and B. Guillaume.A \u03bb-calculus with explicit weakening and explicit substitutions.Mathematical Structures in Computer Science 11(1), 2001.","DOI":"10.1017\/S0960129500003224"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J-P. Jouannaud.Rewrite systems.In J. van Leeuwen, editor,Handbook of Theoretical Computer Science volume B,pages 243\u2013309.North-Holland,1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"3","key":"10_CR14","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1093\/logcom\/10.3.323","volume":"10","author":"J Glauert","year":"2000","unstructured":"J. Glauert, R. Kennaway,and Z. Khasidashvili.Stable results and relative normalization.Journal of Logic and Computation, 10(3),2000.","journal-title":"Journal of Logic and Computation"},{"key":"10_CR15","unstructured":"G. Huet and J-J. L\u00e9vy.Computations in orthogonal rewriting systems. In J.L. Lassez and G.D. Plotkin,editors,Computational Logic; Essays in honor of Alan Robinson pages 394\u201343.MIT Press,1991."},{"key":"10_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Functional back-ends within the lambda-sigma calculus","author":"Th. Hardin","year":"1996","unstructured":"Th. Hardin, L. Maranget, and P. Pagano.Functional back-ends within the lambda-sigma calculus.In Proceedings of the International Conference on Functional Programming LNCS.Springer-Verlag,1996."},{"key":"10_CR17","unstructured":"J.W. Klop.Combinatory Reduction Systems. PhD thesis,CWI,Amsterdam, 1980.Mathematical Centre Tracts n.127."},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"J.W. Klop.Term rewriting systems.Handbook of Logic in Computer Science 2:1\u201316,1992.","DOI":"10.1093\/oso\/9780198537618.003.0001"},{"issue":"1\u20132","key":"10_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"J.W. Klop, V. van Oostrom,and F. van Raamsdonk.Combinatory Reduction Systems:introduction and survey.Theoretical Computer Science, 121(1\u20132):279\u201308,1993.","journal-title":"Theoretical Computer Science"},{"key":"10_CR20","series-title":"Lect Notes Comput Sci","volume-title":"A \u03bb\u2013calculus \u00e0 la de Bruijn with explicit substitutions","author":"F. Kamareddine","year":"1995","unstructured":"F. Kamareddine and A. R\u00edos. A \u03bb\u2013calculus \u00e0 la de Bruijn with explicit substitutions.In Proceedings of the International Symposium on Programming Language Implementation and Logic Programming (PLILP), number982 in LNCS.Springer Verlag,1995."},{"key":"10_CR21","unstructured":"J-J. L\u00e9vy.R\u00e9ductions correctes et optimales dans le lambda-calcul PhD thesis,Universit\u00e9 Paris VII,1978."},{"key":"10_CR22","unstructured":"L. Maranget.La strat\u00e9gie paresseuse PhD thesis,Universit\u00e9 Paris VII, 1992."},{"key":"10_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Typed \u03bb\u2013calculi with explicit substitutions may not terminate","author":"P-A. Melli\u00e8s","year":"1995","unstructured":"P-A. Melli\u00e8s.Typed \u03bb\u2013calculi with explicit substitutions may not terminate.In Proceedings of Typed Lambda Calculi and Applications, number 902in LNCS.Springer-Verlag,1995."},{"key":"10_CR24","unstructured":"P-A. Melli\u00e8s.Description Abstraite des Syst\u00e8mes de R\u00e9\u00e9criture. PhD thesis,Universit\u00e9 Paris VII,1996."},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"P-A. Melli\u00e8s.Axiomatic Rewriting Theory II:The \u03bb\u03c3-calculus enjoys finite normalisation cones.Journal of Logic and Computation 10(3):461\u2013487,2000.","DOI":"10.1093\/logcom\/10.3.461"},{"key":"10_CR26","unstructured":"D. Miller.A logic programming language with lambda-abstraction,function variables,and simple unification.In P. Schroeder-Heister,editor, Proceedings of the International Workshop on Extensions of Logic Pro-gramming, FRG, 1989 number 475 in Lecture Notes in Artificial Intelligence.Springer-Verlag,December 1991."},{"key":"10_CR27","unstructured":"T. Nipkow.Higher-order critical pairs.In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press,July 1991."},{"key":"10_CR28","unstructured":"V.van Oostrom.Confluence for Abstract and Higher-order Rewriting PhD thesis,Vrije University,1994."},{"key":"10_CR29","series-title":"Lect Notes Comput Sci","volume-title":"Normalization in weakly orthogonal rewriting","author":"V. van Oostrom","year":"1999","unstructured":"V.van Oostrom. Normalization in weakly orthogonal rewriting.In Pro-ceedings of the 10th International Conference on Rewriting Techniques and Applications, number 1631 in LNCS.Springer-Verlag,1999."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,15]],"date-time":"2024-02-15T01:40:03Z","timestamp":1707961203000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36576-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}