{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:30:32Z","timestamp":1778301032820,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540582335","type":"print"},{"value":"9783540485797","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"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":[[1994]]},"DOI":"10.1007\/3-540-58233-9_13","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:38:19Z","timestamp":1330252699000},"page":"276-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Comparing combinatory reduction systems and higher-order rewrite systems"],"prefix":"10.1007","author":[{"given":"Vincent","family":"van Oostrom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Femke","family":"van Raamsdonk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"13_CR1","unstructured":"A. Asperti and Laneve C. Interaction systems I: the theory of optimal reductions. Technical Report 1748, INRIA-Rocquencourt, September 1992."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. In Proceedings of the ACM Conference on Principles of Programming Languages, San Francisco, 1990.","DOI":"10.1145\/96709.96712"},{"key":"13_CR3","unstructured":"Peter Aczel. A general Church-Rosser theorem. Technical report, University of Manchester, July 1978."},{"key":"13_CR4","unstructured":"H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, revised edition, 1984. (Second printing 1985)."},{"key":"13_CR5","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science","year":"1993","unstructured":"M. Bezem and J.F. Groote, editors. Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, Utrecht, The Netherlands, March 1993. Springer-Verlag."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization and confluence. In Proceedings of the 16th International Colloquium on Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, pages 137\u2013150, 1989.","DOI":"10.1007\/BFb0035757"},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1090\/S0002-9947-1978-0489603-9","volume":"240","author":"R. Hindley","year":"1978","unstructured":"R. Hindley. Reductions of residuals are finite. Transactions of the American Mathematical Society, 240:345\u2013361, June 1978.","journal-title":"Transactions of the American Mathematical Society"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"S. Kahrs. Context rewriting. In M. Rusinowitch and J.L. R\u00e9my, editors, Proceedings of the Third International Workshop on Conditional and Typed Rewriting Systems, pages 21\u201335, 1992.","DOI":"10.1007\/3-540-56393-8_2"},{"key":"13_CR9","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, Tbilisi, 1990.","journal-title":"Proceedings of I. Vekua Institute of Applied Mathematics"},{"key":"13_CR10","series-title":"PhD Thesis","volume-title":"Mathematical Centre Tracts Nr. 127","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts Nr. 127. CWI, Amsterdam, 1980. PhD Thesis."},{"issue":"1\u20132","key":"13_CR11","doi-asserted-by":"crossref","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\u2013308, December 1993.","journal-title":"Theoretical Computer Science"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Yves Lafont. Interaction nets. In Proceedings 17th ACM Symposium on Principles of Programming Languages, pages 95\u2013108, 1990.","DOI":"10.1145\/96709.96718"},{"key":"13_CR13","unstructured":"C. Laneve. Optimality and Concurrency in Interaction Systems. PhD thesis, dipartimento di informatica universit\u00e0 di pisa, March 1993."},{"key":"13_CR14","unstructured":"Amsterdam, The Netherlands. Proceedings of the sixth annual IEEE Symposium on Logic in Computer Science, Los Alamitos, July 1991. IEEE Computer Society Press."},{"key":"13_CR15","volume-title":"volume 475 of Lecture Notes in Artificial Intelligence","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In [Sie91]."},{"key":"13_CR16","unstructured":"T. Nipkow. Higher-order critical pairs. In [LIC91]."},{"key":"13_CR17","volume-title":"Orthogonal Higher-Order Rewrite Systems are Confluent","author":"T. Nipkow","year":"1993","unstructured":"T. Nipkow. Orthogonal Higher-Order Rewrite Systems are Confluent. In [BG93]."},{"key":"13_CR18","unstructured":"G. Nadathur and D. Miller. An overview of \u03bbProlog. In R.A. Kowalski and K.A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, pages 810\u2013827. MIT Press, 1988."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"V. van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 1994.","DOI":"10.1016\/0304-3975(92)00023-K"},{"key":"13_CR20","unstructured":"V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, March 1994."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Technical Report CS-R9361, CWI, September 1993. also available as VU technical Report IR-333.","DOI":"10.1007\/3-540-58233-9_13"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In Proceedings of the Symposium on Logical Foundations of Computer Science 1994, 1994. to appear.","DOI":"10.1007\/3-540-58140-5_35"},{"key":"13_CR23","unstructured":"L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013385. Academic Press, 1990."},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"F. van Raamsdonk. Confluence and superdevelopments. In C. Kirchner, editor, Proceedings of the 5th International Conference on Rewrite Techniques and Applications, 1993.","DOI":"10.1007\/978-3-662-21551-7_14"},{"issue":"1","key":"13_CR25","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B. K. Rosen","year":"1973","unstructured":"Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the Association for Computing Machinery, 20(1):160\u2013187, January 1973.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"13_CR26","volume-title":"Extensions of Logic Programming, volume 475 of Lecture Notes in Artificial Intelligence","author":"J. Siekmann","year":"1991","unstructured":"J. Siekmann, editor. Extensions of Logic Programming, volume 475 of Lecture Notes in Artificial Intelligence. T\u00fcbingen, FRG, Springer-Verlag, December 1991."},{"key":"13_CR27","volume-title":"\u03bb-calculi with conditional rules","author":"M. Takahashi","year":"1993","unstructured":"M. Takahashi. \u03bb-calculi with conditional rules. In [BG93]."},{"key":"13_CR28","unstructured":"D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993."}],"container-title":["Lecture Notes in Computer Science","Higher-Order Algebra, Logic, and Term Rewriting"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58233-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:21:40Z","timestamp":1778250100000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-58233-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582335","9783540485797"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-58233-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}