{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T05:10:06Z","timestamp":1746335406802,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662445211"},{"type":"electronic","value":"9783662445228"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44522-8_21","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T10:12:23Z","timestamp":1407838343000},"page":"244-255","source":"Crossref","is-referenced-by-count":0,"title":["Relating Nominal and Higher-Order Rewriting"],"prefix":"10.1007","author":[{"given":"Jes\u00fas","family":"Dom\u00ednguez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and all that. CUP (1988)"},{"key":"21_CR2","unstructured":"Dershowitz, N.: Terese: Term Rewrite Systems. CAMTCS, vol.\u00a055. CUP (2003)"},{"key":"21_CR3","unstructured":"Barendregt, H.P.: The Lambda Calculus, its Syntax and Semantics, Revised edn. Studies in Log. and the Found. of Math. North-Holland, vol.\u00a0103 (1984)"},{"key":"21_CR4","unstructured":"Klop, J.W.: Combinatory reduction systems. PhD thesis, Utrecht University (1980)"},{"key":"21_CR5","doi-asserted-by":"publisher","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. Theor. Comp. Sci.\u00a0121, 279\u2013308 (1993)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: LICS, pp, 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"21_CR7","unstructured":"Khasidashvili, Z.: Expression reduction systems. In: Proc. of I. Vekua Institute of Applied Mathematics, vol.\u00a036, pp. 200\u2013220 (1990)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Glauert, J., Kesner, D., Khasidashvili, Z.: Expression reduction systems and extensions: An overview. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes... (Klop Festschrift). LNCS, vol.\u00a03838, pp. 496\u2013553. Springer, Heidelberg (2005)","DOI":"10.1007\/11601548_22"},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comp. Sci.\u00a0192(1), 3\u201329 (1998)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-11999-6_5","volume-title":"Functional and Constraint Logic Programming","author":"M. Hamana","year":"2010","unstructured":"Hamana, M.: Semantic labelling for proving termination of combinatory reduction systems. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol.\u00a05979, pp. 62\u201378. Springer, Heidelberg (2010)"},{"key":"21_CR11","unstructured":"Nipkow, T., Prehofer, C.: Higher-order rewriting and equational reasoning. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction \u2014 A Basis for Applications. Volume I: Foundations. J. of App. Log., vol.\u00a08, pp. 399\u2013430. Kluwer (1998)"},{"issue":"3-5","key":"21_CR12","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M.J. Gabbay","year":"2002","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing\u00a013(3-5), 341\u2013363 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186, 165\u2013193 (2003)","journal-title":"Information and Computation"},{"issue":"6","key":"21_CR14","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","volume":"205","author":"M. Fern\u00e1ndez","year":"2007","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J.: Nominal rewriting. Inf. Comput.\u00a0205(6), 917\u2013965 (2007)","journal-title":"Inf. Comput."},{"issue":"13","key":"21_CR15","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C. Urban","year":"2004","unstructured":"Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theor. Comp. Sci.\u00a0323(13), 473\u2013497 (2004)","journal-title":"Theor. Comp. Sci."},{"key":"21_CR16","unstructured":"Calv\u00e8s, C., Fern\u00e1ndez, M.: Matching and alpha-equivalence check for nominal terms. J. of Comp. and Syst. Sci. (2009); Special issue: Selected papers from WOLLIC 2008"},{"key":"21_CR17","unstructured":"Cheney, J.: Relating nominal and higher-order pattern unification. In: Proc. of UNIF, pp. 104\u2013119 (2005)"},{"key":"21_CR18","first-page":"108","volume-title":"Proc. of 6th ACM SIGPLAN, PPDP 2004","author":"M. Fern\u00e1ndez","year":"2004","unstructured":"Fern\u00e1ndez, M., Gabbay, M.J., Mackie, I.: Nominal rewriting systems. In: Proc. of 6th ACM SIGPLAN, PPDP 2004, pp. 108\u2013119. ACM, New York (2004)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Levy, J., Villaret, M.: Nominal unification from a higher-order perspective. ACM Trans. Comput. Logic\u00a013(2), 10:1\u201310:31 (2012)","DOI":"10.1145\/2159531.2159532"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-31585-5_21","volume-title":"Automata, Languages, and Programming","author":"M. Fern\u00e1ndez","year":"2012","unstructured":"Fern\u00e1ndez, M., Rubio, A.: Nominal completion for rewrite systems with binders. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol.\u00a07392, pp. 201\u2013213. Springer, Heidelberg (2012)"},{"key":"21_CR21","unstructured":"Dom\u00ednguez, J.: A tool to apply nominal recursive path ordering to nominal rules (2014), http:\/\/www.inf.kcl.ac.uk\/pg\/domijesu\/nrpo.tgz"},{"key":"21_CR22","unstructured":"Dom\u00ednguez, J.: A tool to translate between closed nominal rewriting systems and combinatory reduction systems (2014), http:\/\/www.inf.kcl.ac.uk\/pg\/domijesu\/NRS2CRS.tar.gz"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-58233-9_13","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V., van Raamsdonk, F.: Comparing combinatory reduction systems and higher-order rewrite systems. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816, pp. 276\u2013304. Springer, Heidelberg (1994)"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Bertolissi, C., Cirstea, H., Kirchner, C.: Expressing combinatory reduction systems derivations in the rewriting calculus. Higher-Ord. and Symb. Comp.\u00a019, 00110869 (2006)","DOI":"10.1007\/s10990-006-0479-z"},{"issue":"3","key":"21_CR25","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus \u2014 Part\u00a0I. J. of Pure and App. Logs.\u00a09(3), 427\u2013463 (2001)","journal-title":"J. of Pure and App. Logs."},{"issue":"3","key":"21_CR26","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1093\/jigpal\/9.3.377","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus - Part\u00a0II. IGPL\u00a09(3), 377\u2013410 (2001)","journal-title":"IGPL"},{"key":"21_CR27","unstructured":"Bognar, M.: Contexts in Lambda Calculus. PhD thesis, Vrije Universiteit Amsterdam (2002)"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/3-540-48685-2_17","volume-title":"Rewriting Techniques and Applications","author":"F. Raamsdonk van","year":"1999","unstructured":"van Raamsdonk, F.: Higher-order rewriting. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 220\u2013239. Springer, Heidelberg (1999)"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-21493-6_13","volume-title":"Algebraic Informatics","author":"C. Kop","year":"2011","unstructured":"Kop, C.: Simplifying algebraic functional systems. In: Winkler, F. (ed.) CAI 2011. LNCS, vol.\u00a06742, pp. 201\u2013215. Springer, Heidelberg (2011)"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P.: Higher-order rewriting: Framework, confluence and termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes... (Klop Festschrift). LNCS, vol.\u00a03838, pp. 224\u2013250. Springer, Heidelberg (2005)","DOI":"10.1007\/11601548_14"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44522-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:29:30Z","timestamp":1746332970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44522-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662445211","9783662445228"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44522-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}