{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:27:37Z","timestamp":1725481657137},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402541"},{"type":"electronic","value":"9783540448815"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44881-0_9","type":"book-chapter","created":{"date-parts":[[2007,3,5]],"date-time":"2007-03-05T11:39:56Z","timestamp":1173094796000},"page":"107-122","source":"Crossref","is-referenced-by-count":6,"title":["Expression Reduction Systems with Patterns"],"prefix":"10.1007","author":[{"given":"Julien","family":"Forest","sequence":"first","affiliation":[]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"9_CR2","unstructured":"H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Revised Edition."},{"key":"9_CR3","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-Data-Type Systems. Theoretical Computer Science, 277, 2001."},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","volume-title":"11th RTA","author":"E. Bonelli","year":"2000","unstructured":"E. Bonelli, D. Kesner, and A. R\u00edos. A de Bruijn notation for higher-order rewriting. In 11th RTA, LNCS 1833. 2000."},{"key":"9_CR5","unstructured":"S. Cerrito and D. Kesner. Pattern matching as cut elimination. Theoretical Computer Science. To appear."},{"key":"9_CR6","unstructured":"S. Cerrito and D. Kesner. Pattern matching as cut elimination. In 14th LICS. IEEE. 1999."},{"key":"9_CR7","unstructured":"H. Cirstea. Calcul de r\u00e9\u00e9criture: fondements et applications. Th\u00e8se de doctorat, Universit\u00e9 Henri Poincar\u00e9 \u2014 Nancy 1, 2000."},{"key":"9_CR8","unstructured":"H. Cirstea and C. Kirchner. \u03c1-calculus, the rewriting calculus. In 5th CCL, 1998."},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","volume-title":"13th RTA","author":"J. Forest","year":"2002","unstructured":"J. Forest. A weak calculus with explicit operators for pattern matching and substitution. In 13th RTA, LNCS 2378. 2002."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"J. Forest and D. Kesner. Expression Reduction Systems with Patterns, 2003. Available on http:\/\/www.pps.jussieu.fr\/~kesner\/papers\/ .","DOI":"10.1007\/3-540-44881-0_9"},{"key":"9_CR11","unstructured":"J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In 14th LICS. IEEE. 1999."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"D. Kesner, L. Puel, and V. Tannen. A Typed Pattern Calculus. Information and Computation, 124(1), 1996.","DOI":"10.1006\/inco.1996.0004"},{"key":"9_CR13","unstructured":"Z. Khasidashvili. Expression reduction systems. In Proceedings of IN Vekua Institute of Applied Mathematics, volume 36, Tbilisi, 1990."},{"key":"9_CR14","series-title":"Lect Notes Comput Sci","volume-title":"FOSSACS\u201901","author":"C. Kirchner","year":"2001","unstructured":"C. Kirchner, H. Cirstea and L. Liquori. The Rho Cube. In FOSSACS\u201901, LNCS 2030. 2001."},{"key":"9_CR15","series-title":"Mathematical Centre Tracts","volume-title":"Combinatory Reduction Systems","author":"J.-W. Klop","year":"1980","unstructured":"J.-W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980. PhD Thesis."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"J.-W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121, 1993.","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"9_CR17","unstructured":"T. Nipkow. Higher-order critical pairs. In 6th LICS. IEEE. 1991."},{"key":"9_CR18","unstructured":"The Objective Caml language, http:\/\/caml.inria.fr\/ ."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"M. Takahashi. Parallel Reductions in lambda-Calculus. Journal of Symbolic Computation, 7(2), 1989.","DOI":"10.1016\/S0747-7171(89)80045-8"},{"key":"9_CR20","series-title":"Lect Notes Comput Sci","volume-title":"3rd LFCS","author":"V. Oostrom van","year":"1994","unstructured":"V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In 3rd LFCS, LNCS 813. 1994."},{"key":"9_CR21","series-title":"Lect Notes Comput Sci","volume-title":"12th RTA","author":"F. Raamsdonk van","year":"2001","unstructured":"F. van Raamsdonk. On termination of higher-order rewriting. In 12th RTA, LNCS 2051. 2001."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"D. 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":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44881-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T01:45:42Z","timestamp":1556156742000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44881-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402541","9783540448815"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44881-0_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}