{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T05:16:17Z","timestamp":1736658977557,"version":"3.32.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T00:00:00Z","timestamp":1164931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2006,12]]},"DOI":"10.1007\/s10990-006-0479-z","type":"journal-article","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T18:07:57Z","timestamp":1164650877000},"page":"345-376","source":"Crossref","is-referenced-by-count":3,"title":["Expressing combinatory reduction systems derivations in the rewriting calculus"],"prefix":"10.1007","volume":"19","author":[{"given":"Clara","family":"Bertolissi","sequence":"first","affiliation":[]},{"given":"Horatiu","family":"Cirstea","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"479_CR1","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1017\/S095679689700289X","volume":"7","author":"F. Barbanera","year":"1997","unstructured":"Barbanera, F., Fern\u00e1ndez, M., Geuvers, H.: Modularity of Strong Normalisation and Confluence in the Algebraic \u03b3-cube. J. Funct. Program. 7(6), 613\u2013660 (1997)","journal-title":"J. Funct. Program."},{"key":"479_CR2","unstructured":"Barendregt, H.: Lambda Calculus: its Syntax and Semantics. North Holland (1984)"},{"key":"479_CR3","volume-title":"Principles of Programming Languages\u2014POPL2003","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Patterns Type Systems. In: Principles of Programming Languages\u2014POPL2003, New Orleans, USA. ACM (2003)"},{"key":"479_CR4","doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Definitions by rewriting in the calculus of constructions. In: Logic in Computer Science, pp. 9\u201318 (2001)","DOI":"10.1109\/LICS.2001.932478"},{"key":"479_CR5","unstructured":"Blanqui, F.: Type Theory and Rewriting. Ph.D. thesis, University Paris-Sud (2001)"},{"key":"479_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1941","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1941)","journal-title":"J. Symb. Logic"},{"key":"479_CR7","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Faure, G., Kirchner, C.: A rho-calculus of explicit constraint application. In: Proceedings of WRLA\u201904, vol. 117 of ENTCS (2004)","DOI":"10.1016\/j.entcs.2004.06.029"},{"issue":"3","key":"479_CR8","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus\u2014Part I and II. Logic J. Int. Group Pure Appl. Logic 9(3), 427\u2013498 (2001)","journal-title":"Logic J. Int. Group Pure Appl. Logic"},{"key":"479_CR9","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: Matching power. In: Proceedings of RTA, vol. 2051 of LNCS, pp. 77\u201392, Springer-Verlag (2001)","DOI":"10.1007\/3-540-45127-7_8"},{"key":"479_CR10","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: The rho cube. In: Proc. of FOSSACS, vol. 2030 of LNCS, pp. 166\u2013180 (2001)","DOI":"10.1007\/3-540-45315-6_11"},{"key":"479_CR11","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: Rewriting calculus with(out) types. In: Gadducci, F., Montanari, U. (eds.), Proceedings of WRLA\u201902, Pisa (Italy), ENTCS (2002)."},{"key":"479_CR12","unstructured":"Cirstea, H., Liquori, L., Wack, B.: Typed recursion by pattern matching. In: Proceeding of the TYPES conference (2004)."},{"key":"479_CR13","doi-asserted-by":"crossref","unstructured":"Faure, G., Kirchner, C.: Exceptions in the Rewriting Calculus. In: Proc. of RTA, vol. 2378 of LNCS, pp. 66\u201382 Springer-Verlag (2002).","DOI":"10.1007\/3-540-45610-4_6"},{"key":"479_CR14","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"D. Goldfarb","year":"1981","unstructured":"Goldfarb, D.: The Undecidability of the Second Order Unification Problem. Theor. Comput. Sci. 13, 225\u2013230 (1981)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"479_CR15","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A Unification Algorithm for Typed Lambda Calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"479_CR16","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","volume":"173","author":"J. Jouannaud","year":"1997","unstructured":"Jouannaud, J., Okada, M.: Abstract Data Type Systems. Theor. Comput. Sci. 173(2), 349\u2013391 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"479_CR17","first-page":"200","volume":"36","author":"Z. Khasidashvili","year":"1990","unstructured":"Khasidashvili, Z.: Expression Reduction Systems. In: Proceedings of I. Vekua Ins. Appl. Math., vol. 36, pp. 200\u2013220 (1990)","journal-title":"Proceedings of I. Vekua Ins. Appl. Math."},{"key":"479_CR18","unstructured":"Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, CWI (1980)"},{"key":"479_CR19","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"Klop, J.W., Oostrom, V.V., Raamsdonk, F.V.: Combinatory Reduction Systems: Introduction and Survey. Theor. Comput. Sci. 121, 279\u2013308 (1993)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"479_CR20","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J Logic Comput 1(4), 497\u2013536 (1991)","journal-title":"J Logic Comput"},{"key":"479_CR21","doi-asserted-by":"crossref","unstructured":"Miller, D.A., Nadathur, G.: Higher-order logic programming. In: Shapiro, E. (ed.), Proceedings of the Third International Logic Programming Conference, vol. 225 of LNCS, pp. 448\u2013462, Springer-Verlag, (1986)","DOI":"10.1007\/3-540-16492-8_94"},{"key":"479_CR22","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of Logic in Computer Science, pp. 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"479_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Orthogonal higher-order rewrite systems are confluent. In: Proceedings of the International Conference on Typed La mbda Calculi and Applications, pp. 306\u2013317 (1993)","DOI":"10.1007\/BFb0037114"},{"key":"479_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Prehofer, C.: Higher-Order Rewriting and Equational Reasoning. In: Bibel, W., Schmitt, P. (eds.), Automated Deduction\u2014A Basis for Applications, vol. I: Foundations, Kluwer (1998)","DOI":"10.1007\/978-1-4612-1778-7_4"},{"key":"479_CR25","unstructured":"Pagano, B.: Des calculs de substitution explicites et de leur application la compilation des langages fonctionnels. Ph.D. thesis, U. Paris VI (1997)"},{"key":"479_CR26","doi-asserted-by":"crossref","unstructured":"Qian, Z.: Linear Unification of Higher-Order Patterns. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.), Proceedings of TAPSOFT\u201993, of Lecture Notes in Computer Science, vol. 668, pp. 391\u2013405, Springer-Verlag (1993)","DOI":"10.1007\/3-540-56610-4_78"},{"key":"479_CR27","doi-asserted-by":"crossref","unstructured":"van Oostrom, V., van Raamsdonk, F.: Comparing Combinatory Reduction Systems and Higher-order Rewrite Systems. In: Higher-Order Algebra, Logic and Term Rewriting (HOA), pp. 276\u2013304 (1993)","DOI":"10.1007\/3-540-58233-9_13"},{"key":"479_CR28","doi-asserted-by":"crossref","unstructured":"Wolfram, D.A.: The Clausal Theory of Types, vol. 21 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1993)","DOI":"10.1017\/CBO9780511569906"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-006-0479-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-006-0479-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-006-0479-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T04:49:30Z","timestamp":1736657370000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-006-0479-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12]]}},"alternative-id":["479"],"URL":"https:\/\/doi.org\/10.1007\/s10990-006-0479-z","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}