{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T20:10:01Z","timestamp":1737317401499,"version":"3.33.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T00:00:00Z","timestamp":1184976000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,11,19]]},"DOI":"10.1007\/s10817-007-9083-0","type":"journal-article","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T10:35:28Z","timestamp":1184927728000},"page":"513-541","source":"Crossref","is-referenced-by-count":0,"title":["Expression Reduction Systems with Patterns"],"prefix":"10.1007","volume":"39","author":[{"given":"Julien","family":"Forest","sequence":"first","affiliation":[]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,7,21]]},"reference":[{"key":"9083_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and all that. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"9083_CR2","unstructured":"Barendregt, H.: The lambda calculus: its syntax and semantics, vol. 103. Studies in Logic and the Foundations of Mathematics. North-Holland. Revised Edition (1984)"},{"key":"9083_CR3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"277","author":"F. Blanqui","year":"2002","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive-data-type systems. Theoretical Comput. Sci. 277, 41\u201368 (2002)","journal-title":"Theoretical Comput. Sci."},{"key":"9083_CR4","doi-asserted-by":"crossref","unstructured":"Bonelli, E., Kesner, D., R\u00edos, A.: A de Bruijn notation for higher-order rewriting. In: L. Bachmair (ed.) 11th International Conference on Rewriting Techniques and Applications, vol. 1833 of Lecture Notes in Computer Science. pp. 62\u201379, Springer (2000)","DOI":"10.1007\/10721975_5"},{"key":"9083_CR5","doi-asserted-by":"crossref","unstructured":"Cerrito, S., Kesner, D.: Pattern matching as cut elimination. In: Longo, G. (ed.) 14th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 98\u2013108. IEEE Computer Society Press (1999)","DOI":"10.1109\/LICS.1999.782596"},{"key":"9083_CR6","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.tcs.2004.03.032","volume":"323","author":"S. Cerrito","year":"2004","unstructured":"Cerrito, S., Kesner, D.: Pattern matching as cut elimination. Theoretical Comput. Sci. 323, 71\u2013127 (2004)","journal-title":"Theoretical Comput. Sci."},{"key":"9083_CR7","unstructured":"Cirstea, H., Kirchner, C.: \u03c1-Calculus, the rewriting calculus. In: 5th International Workshop on Constraints in Computational Logics (1998)"},{"key":"9083_CR8","doi-asserted-by":"crossref","unstructured":"Forest, J.: A weak calculus with explicit operators for pattern matching and substitution. In: Tison, S. (ed.) 13th International Conference on Rewriting Techniques and Applications, vol. 2378 of Lecture Notes in Computer Science. pp. 174\u2013191, Springer (2002)","DOI":"10.1007\/3-540-45610-4_13"},{"key":"9083_CR9","doi-asserted-by":"crossref","unstructured":"Forest, J., Kesner, D.: Expression reduction systems with patterns. In: Nieuwenhuis, R. (ed.) 14th International Conference on Rewriting Techniques and Applications, vol. 2706 of Lecture Notes in Computer Science. pp. 107\u2013122, Springer (2003)","DOI":"10.1007\/3-540-44881-0_9"},{"key":"9083_CR10","unstructured":"Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, vol.\u00a04. Prentice Hall, pp. 80\u2013149 (1978)"},{"key":"9083_CR11","doi-asserted-by":"crossref","unstructured":"Huet, G., Oppen, D.: Equations and rewrite rules: a survey. In: Book, R.V. (ed.) Formal Language Theory: Perspectives and Open Problems. Academic, pp. 349\u2013405 (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"9083_CR12","doi-asserted-by":"crossref","unstructured":"Jay, C.B., Kesner, D.: Pure pattern calculus. In: Sestoft, P. (ed.) Proceedings of the European Symposium on Programming (ESOP). LNCS, vol. 3924, pp. 100\u2013114, Vienna, Austria, March\u2013April 2006","DOI":"10.1007\/11693024_8"},{"key":"9083_CR13","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Rubio, A.: The higher-order recursive path ordering. In: Longo, G. (ed.) 14th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 402\u2013411. IEEE Computer Society Press (1999)","DOI":"10.1109\/LICS.1999.782635"},{"key":"9083_CR14","unstructured":"Kahl, W.: Basic pattern matching calculi: syntax, reduction, confluence, and normalisation. Technical Report\u00a016, Software Quality Research Laboratory, McMaster University (2003)"},{"issue":"1","key":"9083_CR15","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1006\/inco.1996.0004","volume":"124","author":"D. Kesner","year":"1996","unstructured":"Kesner, D., Puel, L., Tannen, V.: A typed pattern calculus. Inf. Comput. 124(1), 32\u201361 (1996)","journal-title":"Inf. Comput."},{"key":"9083_CR16","unstructured":"Khasidashvili, Z.: Expression reduction systems. In: Proceedings of IN Vekua Institute of Applied Mathematics, vol.\u00a036. Tbilisi (1990)"},{"key":"9083_CR17","unstructured":"Klop, J.-W.: Combinatory reduction systems, vol. 127 of Mathematical Centre Tracts. Amsterdam, Mathematisch Centrum. Ph.D. thesis (1980)"},{"key":"9083_CR18","unstructured":"Klop, J.-W.: Term rewriting systems, vol.\u00a02. Oxford University Press (1992)"},{"key":"9083_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., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121, 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"key":"9083_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: 6th Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"issue":"7","key":"9083_CR21","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0747-7171(89)80045-8","volume":"2","author":"M. Takahashi","year":"1989","unstructured":"Takahashi, M.: Parallel reductions in Lambda-Calculus. J. Symbolic Comput. 2(7), 113\u2013123 (1989)","journal-title":"J. Symbolic Comput."},{"key":"9083_CR22","unstructured":"van Oostrom, V.: Lambda calculus with patterns. Technical Report IR-228, Vrije Universiteit, Amsterdam (1990)"},{"key":"9083_CR23","doi-asserted-by":"crossref","unstructured":"van Oostrom, V., van Raamsdonk, F.: Weak orthogonality implies confluence: the higher-order case. In: Nerode, A., Matiyasevich, Y. (eds.) Proceedings of the 3rd International Symposium on Logical Foundations of Computer Science, vol. 813 of Lecture Notes in Computer Science. pp. 379\u2013392, Springer-Verlag (1994)","DOI":"10.1007\/3-540-58140-5_35"},{"key":"9083_CR24","doi-asserted-by":"crossref","unstructured":"van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) 12th International Conference on Rewriting Techniques and Applications, vol. 2051 of Lecture Notes in Computer Science. pp. 261\u2013275, Springer (2001)","DOI":"10.1007\/3-540-45127-7_20"},{"key":"9083_CR25","doi-asserted-by":"crossref","unstructured":"Wolfram, D.: The Clausal Theory of Types, vol.\u00a021 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (1993)","DOI":"10.1017\/CBO9780511569906"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9083-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9083-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9083-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T19:44:37Z","timestamp":1737315877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9083-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,21]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,11,19]]}},"alternative-id":["9083"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9083-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2007,7,21]]}}}