{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:51Z","timestamp":1761596871063},"reference-count":23,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80674-1","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"28-44","source":"Crossref","is-referenced-by-count":4,"title":["Translating Combinatory Reduction Systems into the Rewriting Calculus"],"prefix":"10.1016","volume":"86","author":[{"given":"Clara","family":"Bertolissi","sequence":"first","affiliation":[]},{"given":"Horatiu","family":"Cirstea","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"6","key":"10.1016\/S1571-0661(04)80674-1_NEWBIB1","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1017\/S095679689700289X","article-title":"Modularity of Strong Normalisation and Confluence in the Algebraic \u03bb-Cube","volume":"7","author":"Barbanera","year":"1997","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB2","series-title":"Lambda Calculus: its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB3","series-title":"Principles of Programming Languages - POPL 2003","article-title":"Pure Patterns Type Systems","author":"Barthe","year":"2003"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB4","doi-asserted-by":"crossref","unstructured":"C. Bertolissi, H. Cirstea, and C. Kirchner. Translating Combinatory Reduction Systems into the Rewriting Calculus. Technical Report A03-R-057, LORIA, June 2003. http:\/\/www.loria.fr\/~bertolis\/A03-R-057.ps.","DOI":"10.1016\/S1571-0661(04)80674-1"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB5","doi-asserted-by":"crossref","unstructured":"F. Blanqui. Type Theory and Rewriting. PhD thesis, University Paris-Sud, 2001.","DOI":"10.1109\/LICS.2001.932478"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A Formulation of the Simple Theory of Types","volume":"5","author":"Church","year":"1941","journal-title":"Journal of Symbolic Logic"},{"issue":"3","key":"10.1016\/S1571-0661(04)80674-1_NEWBIB7","first-page":"427","article-title":"The rewriting calculus \u2014 Part I and II","volume":"9","author":"Cirstea","year":"2001","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB8","doi-asserted-by":"crossref","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. Matching Power. In Proc. of RTA, volume 2051 of LNCS, pages 77\u201392. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45127-7_8"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB9","doi-asserted-by":"crossref","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. The Rho Cube. In Proc. of FOSSACS, volume 2030 of LNCS, pages 166\u2013180, 2001.","DOI":"10.1007\/3-540-45315-6_11"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB10","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. Rewriting calculus with(out) types. In F. Gadducci and U. Montanari, editors, Proceedings of the fourth workshop on rewriting logic and applications, Pisa (Italy), September 2002. Electronic Notes in Theoretical Computer Science."},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB11","doi-asserted-by":"crossref","unstructured":"G. Faure and C. Kirchner. Exceptions in the Rewriting Calculus. In Proc. of RTA, volume 2378 of LNCS, pages 66\u201382. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45610-4_6"},{"issue":"2","key":"10.1016\/S1571-0661(04)80674-1_NEWBIB12","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","article-title":"Abstract Data Type Systems","volume":"173","author":"Jouannaud","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB13","unstructured":"Z. Khasidashvili. Expression reduction systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200\u2013220, 1990."},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB14","unstructured":"Z. Khasidashvili. Church-rosser theorem in orthogonal reduction systems. Technical report, INRIA Rocquencourt, 1992."},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB15","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","article-title":"Combinatory Reduction Systems: Introduction and Survey","volume":"121","author":"Klop","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB16","unstructured":"J. W. Klop. Combinatory Reduction Systems. PhD thesis, CWI, 1980."},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB17","doi-asserted-by":"crossref","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Proc. of ELP, volume 475 of LNCS, pages 253\u2013281. Springer-Verlag, 1991.","DOI":"10.1007\/BFb0038698"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB18","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proceedings of Logic in Computer Science, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB19","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Orthogonal higher-order rewrite systems are confluent. In Proceedings of the International Conference on Typed La mbda Calculi and Applications, pages 306\u2013317, 1993.","DOI":"10.1007\/BFb0037114"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB20","article-title":"Higher-Order Rewriting and Equational Reasoning","volume":"Volume I","author":"Nipkow","year":"1998"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB21","unstructured":"B. Pagano. Des calculs de substitution explicites et de leur application \u00e0 la compilation des langages fonctionnels. PhD thesis, U. Paris VI, 1997."},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB22","doi-asserted-by":"crossref","unstructured":"V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Report CS-R9361, CWI, september 1993.","DOI":"10.1007\/3-540-58233-9_13"},{"key":"10.1016\/S1571-0661(04)80674-1_NEWBIB23","doi-asserted-by":"crossref","unstructured":"D. A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511569906"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806741?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806741?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:25Z","timestamp":1585898065000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806741"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066104806741"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80674-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}