{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:22Z","timestamp":1761611182666,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054249","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"72-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["X.R.S: Explicit reduction systems \u2014 A first-order calculus for higher-order calculi"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Pagano","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. In Principles of Programming Languages, pages 31\u201346, 1990.","DOI":"10.1145\/96709.96712"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1017\/S0960129500000566","volume":"4","author":"A. Asperti","year":"1994","unstructured":"A. Asperti and C. Laneve. Interaction systems 1: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457\u2013504, 1994.","journal-title":"Mathematical Structures in Computer Science"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"R. Bloo and K.H. Rose. Combinatory reduction systems with explicit substitution that preserve strong normalisation. In Rewriting Techniques and Applications, pages 169\u2013183, 1996.","DOI":"10.1007\/3-540-61464-8_51"},{"issue":"2","key":"10_CR4","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, March 1996.","journal-title":"Journal of the ACM"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"P.-L. Curien. An abstract framework for environment machines. Theoretical Computer Science, 82, 1991.","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"10_CR6","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In Logic in Computer Science, 1995."},{"key":"10_CR7","unstructured":"G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: the case of higher-order patterns. In Logic Programming, pages 259\u2013273, 1996."},{"key":"10_CR8","unstructured":"J. Goubault. Weak normalization of \u03bb\u03c3-calculus. GDR-AMI, 1997."},{"key":"10_CR9","unstructured":"T. Hardin and J.-J. L\u00e9vy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"T. Hardin, L. Maranget, and B. Pagano. Functional back-ends within the lambda-sigma calculus. In International Conference on Functional Programming, pages 25\u201333, 1996.","DOI":"10.1145\/232629.232632"},{"key":"10_CR11","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61464-8_52","volume":"1103","author":"D. Kesner","year":"1996","unstructured":"D. Kesner. Confluence properties of extensional and non-extensional lambda-calculi with explicit substitutions. Lecture Notes in Computer Science, 1103:184\u2013--, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"10_CR12","first-page":"200","volume":"36","author":"Z.O. Khasidashvili","year":"1990","unstructured":"Z.O. Khasidashvili. Expression reduction systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200\u2013220, 1990.","journal-title":"Proceedings of I. Vekua Institute of Applied Mathematics"},{"key":"10_CR13","unstructured":"J.W. Klop. Combinatory Reduction Systems. PhD thesis, University of Amsterdam, 1980."},{"key":"10_CR14","unstructured":"J.W. Klop. Term rewriting systems. Technical report, Centrum voor Wiskunde en Informatica, 1990."},{"key":"10_CR15","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/3-540-61756-6_98","volume":"1140","author":"F. Kamareddine","year":"1996","unstructured":"F. Kamareddine and A. Rios. Generalized-reduction and explicit substitution. Lecture Notes in Computer Science, 1140:378\u2013--, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From \u03bb\u03c3 to \u03bb\u03c5: A journey through calculi of explicit substitutions. In Principles of Programming Languages, pages 60\u201369, 1994.","DOI":"10.1145\/174675.174707"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"P.-A. Mellies. Typed lambda-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, pages 497\u2013536, 1991.","DOI":"10.1093\/logcom\/1.4.497"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0020-0190(92)90155-O","volume":"41","author":"F. M\u00fcller","year":"1992","unstructured":"F. M\u00fcller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41:293\u2013299, 1992.","journal-title":"Information Processing Letters"},{"key":"10_CR20","volume-title":"Technical Report RR-3107","author":"C. Mu\u00f1oz","year":"1997","unstructured":"C. Mu\u00f1oz. Meta-theoretical properties of \u03bb \u03c6 : A left-linear variant of \u03bb \u03c3 . Technical Report RR-3107, Unit\u00e9 de recherche INRIA-Rocquencourt, F\u00e9vrier 1997."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proceedings of Logic in Computer Science, pages 342\u2013349, 1993.","DOI":"10.1109\/LICS.1991.151658"},{"key":"10_CR22","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/3-540-58140-5_35","volume":"813","author":"V. Oostrom","year":"1994","unstructured":"V. Oostrom and F. Raamsdonk. Weak orthogonality implies confluence: The higher-order case. Lecture Notes in Computer Science, 813:379\u2013--, 1994.","journal-title":"Lecture Notes in Computer Science"},{"key":"10_CR23","unstructured":"A. Rios. Contributions \u00e0 l'\u00e9tude des Lambda-calculs avec Substitutions Explicites. PhD thesis, Universit\u00e9 PARIS 7, 1993."},{"key":"10_CR24","unstructured":"K. H. Rose and R. R. Moore. Xy-pic Reference Manual, 1995."},{"key":"10_CR25","unstructured":"F. van Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, University of Amsterdam, 1996."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054249","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T07:19:52Z","timestamp":1736407192000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0054249","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}