{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:20Z","timestamp":1765617740788,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":104,"publisher":"ACM","funder":[{"name":"Royal Society (International Exchanges)","award":["IES\\\\R2\\\\212106"],"award-info":[{"award-number":["IES\\\\R2\\\\212106"]}]},{"name":"Leverhulme Trust","award":["VP2-2021-019"],"award-info":[{"award-number":["VP2-2021-019"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756921","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing Languages with Binding Operators in Rewriting Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8325-5815","authenticated-orcid":false,"given":"Maribel","family":"Fernandez","sequence":"first","affiliation":[{"name":"King's College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4779-3848","authenticated-orcid":false,"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Urbana, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_2"},{"key":"e_1_3_3_2_4_2","unstructured":"Peter Aczel. [n. d.]. A general Church-Rosser theorem. ([n. d.]). Manuscript University of Manchester 1978."},{"key":"e_1_3_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Guillaume Allais Robert Atkey James Chapman Conor McBride and James McKinna. 2018. A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2 ICFP Article 90 (jul 2018) 30\u00a0pages. 10.1145\/3236785","DOI":"10.1145\/3236785"},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"crossref","unstructured":"Musab\u00a0A. AlTurki and Jos\u00e9 Meseguer. 2015. Executable rewriting logic semantics of Orc and formal analysis of Orc programs. J. Log. Algebr. Meth. Program. 84 4 (2015) 505\u2013533.","DOI":"10.1016\/j.jlamp.2015.03.003"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Mauricio Ayala-Rinc\u00f3n Washington de Carvalho\u00a0Segundo Maribel Fern\u00e1ndez Daniele Nantes-Sobrinho and Ana Oliveira. 2019. A formalisation of nominal \u03b1-equivalence with A C and AC symbols. Theor. Comput. Sci. 781 (2019) 3\u201323. 10.1016\/j.tcs.2019.02.020","DOI":"10.1016\/j.tcs.2019.02.020"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Mauricio Ayala-Rinc\u00f3n Washington de Carvalho\u00a0Segundo Maribel Fern\u00e1ndez Gabriel\u00a0Ferreira Silva and Daniele Nantes-Sobrinho. 2021. Formalising nominal C-unification generalised with protected variables. Math. Struct. Comput. Sci. 31 3 (2021) 286\u2013311. 10.1017\/S0960129521000050","DOI":"10.1017\/S0960129521000050"},{"key":"e_1_3_3_2_9_2","first-page":"11","volume-title":"1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016","author":"Ayala-Rinc\u00f3n Mauricio","year":"2016","unstructured":"Mauricio Ayala-Rinc\u00f3n, Maribel Fern\u00e1ndez, and Daniele Nantes-Sobrinho. 2016. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 11."},{"key":"e_1_3_3_2_10_2","series-title":"(LNCS)","volume-title":"TPHOL 18","author":"Aydemier B.\u00a0E.","year":"2005","unstructured":"B.\u00a0E. Aydemier, A. Bohannon, M. Fairbairn, J.\u00a0N. Foster, B.\u00a0C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, , and S. Zdancewic. 2005. Mechanized metatheory for the masses: The POPLmark challenge. In TPHOL 18(LNCS). Springer."},{"key":"e_1_3_3_2_11_2","first-page":"228","volume-title":"Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS \u201988), Edinburgh, Scotland, UK, July 5-8, 1988","author":"Bachmair Leo","year":"1988","unstructured":"Leo Bachmair. 1988. Proof by Consistency in Equational Theories. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS \u201988), Edinburgh, Scotland, UK, July 5-8, 1988. IEEE Computer Society, 228\u2013233."},{"key":"e_1_3_3_2_12_2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Nachum Dershowitz. 1989. Completion for Rewriting Modulo a Congruence. Theor. Comput. Sci. 67 2&3 (1989) 173\u2013201.","DOI":"10.1016\/0304-3975(89)90003-0"},{"key":"e_1_3_3_2_13_2","series-title":"LIPIcs","first-page":"81","volume-title":"Rewriting Techniques and Applications (RTA\u201913)","author":"Bae Kyungmin","year":"2013","unstructured":"Kyungmin Bae, Santiago Escobar, and Jos\u00e9 Meseguer. 2013. Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In Rewriting Techniques and Applications (RTA\u201913)(LIPIcs, Vol.\u00a021). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 81\u201396."},{"key":"e_1_3_3_2_14_2","doi-asserted-by":"crossref","unstructured":"Kyungmin Bae and Jos\u00e9 Meseguer. 2015. Model checking linear temporal logic of rewriting formulas under localized fairness. Sci. Comput. Program. 99 (2015) 193\u2013234.","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"e_1_3_3_2_15_2","volume-title":"The Lambda Calculus, its Syntax and Semantics","author":"Barendregt H.\u00a0P.","year":"1984","unstructured":"H.\u00a0P. Barendregt. 1984. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 2nd ed."},{"key":"e_1_3_3_2_16_2","doi-asserted-by":"crossref","unstructured":"D. Basin M. Clavel and J. Meseguer. 2004. Rewriting Logic as a Metalogical Framework. ACM Transactions on Computational Logic 5 (2004) 528\u2013576. Issue 3.","DOI":"10.1145\/1013560.1013566"},{"key":"e_1_3_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Jasmin\u00a0Christian Blanchette Lorenzo Gheri Andrei Popescu and Dmitriy Traytel. 2019. Bindings as bounded natural functors. Proc. ACM Program. Lang. 3 POPL (2019) 22:1\u201322:34. 10.1145\/3290335","DOI":"10.1145\/3290335"},{"key":"e_1_3_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Adel Bouhoula and Micha\u00ebl Rusinowitch. 1995. Implicit Induction in Conditional Theories. J. Autom. Reason. 14 2 (1995) 189\u2013235. 10.1007\/BF00881856","DOI":"10.1007\/BF00881856"},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Roberto Bruni and Jos\u00e9 Meseguer. 2006. Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360 1-3 (2006) 386\u2013414.","DOI":"10.1016\/j.tcs.2006.04.012"},{"key":"e_1_3_3_2_21_2","doi-asserted-by":"crossref","unstructured":"Christophe Calv\u00e8s and Maribel Fern\u00e1ndez. 2008. A Polynomial Nominal Unification Algorithm. Theor. Comp. Sci. 403 (Aug. 2008) 285\u2013306. Issue 2\u20133.","DOI":"10.1016\/j.tcs.2008.05.012"},{"key":"e_1_3_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Christophe Calv\u00e8s and Maribel Fern\u00e1ndez. 2010. Matching and Alpha-equivalence Check for Nominal Terms. Journal of Comp. Syst. Sci. 76 5 (2010) 283\u2013301.","DOI":"10.1016\/j.jcss.2009.10.003"},{"key":"e_1_3_3_2_23_2","series-title":"LNCS","first-page":"234","volume-title":"Logic-Based Program Synthesis and Transformation - 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers","author":"Calv\u00e8s Christophe","year":"2011","unstructured":"Christophe Calv\u00e8s and Maribel Fern\u00e1ndez. 2011. The First-Order Nominal Link. In Logic-Based Program Synthesis and Transformation - 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers(LNCS, Vol.\u00a06564). Springer, 234\u2013248."},{"key":"e_1_3_3_2_24_2","first-page":"104","volume-title":"Proceedings of the 19th International Workshop on Unification (UNIF 2005)","author":"Cheney James","year":"2005","unstructured":"James Cheney. 2005. Relating Nominal and Higher-Order Pattern Unification. In Proceedings of the 19th International Workshop on Unification (UNIF 2005). 104\u2013119."},{"key":"e_1_3_3_2_25_2","doi-asserted-by":"crossref","unstructured":"Alonzo Church. 1941. The Calculi of Lambda-Conversion. Annals of Mathematics Studies 6 (1941). Second edition 1951.","DOI":"10.2307\/2267126"},{"key":"e_1_3_3_2_26_2","volume-title":"Proc. of the CafeOBJ Symposium \u201998, Numazu, Japan","author":"Clavel Manuel","year":"1998","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, and Jos\u00e9 Meseguer. 1998. Building equational proving tools by reflection in rewriting logic. In Proc. of the CafeOBJ Symposium \u201998, Numazu, Japan. CafeOBJ Project. http:\/\/maude.cs.uiuc.edu."},{"key":"e_1_3_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/1808998"},{"key":"e_1_3_3_2_28_2","doi-asserted-by":"crossref","unstructured":"Manuel Clavel Jos\u00e9 Meseguer and Miguel Palomino. 2007. Reflection in Membership Equational Logic Many-Sorted Equational Logic Horn Logic with Equality and Rewriting Logic. Theoretical Computer Science 373 (2007) 70\u201391.","DOI":"10.1016\/j.tcs.2006.12.009"},{"key":"e_1_3_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Ranald\u00a0A. Clouston and Andrew\u00a0M. Pitts. 2007. Nominal Equational Logic. ENTCS 172 (2007) 223\u2013257. 10.1016\/j.entcs.2007.02.009","DOI":"10.1016\/j.entcs.2007.02.009"},{"key":"e_1_3_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Hubert Comon and Robert Nieuwenhuis. 2000. Induction=I-Axiomatization+First-Order Consistency. Inf. Comput. 159 1-2 (2000) 151\u2013186.","DOI":"10.1006\/inco.2000.2875"},{"key":"e_1_3_3_2_31_2","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and Gerard Huet. 1988. The Calculus of Constructions. Information and Computation 76 2\u20133 (Feb. 1988) 95\u2013120.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_3_2_32_2","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, Vol. B","author":"Dershowitz N.","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. 1990. Rewrite Systems. In Handbook of Theoretical Computer Science, Vol. B, J.\u00a0van Leeuwen (Ed.). North-Holland, 243\u2013320."},{"key":"e_1_3_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Francisco Dur\u00e1n and Jos\u00e9 Meseguer. 2003. Structured theories and institutions. Theor. Comput. Sci. 309 1-3 (2003) 357\u2013380.","DOI":"10.1016\/S0304-3975(03)00312-8"},{"key":"e_1_3_3_2_34_2","doi-asserted-by":"crossref","unstructured":"Francisco Dur\u00e1n and Jos\u00e9 Meseguer. 2007. Maude\u2019s module algebra. Sci. Comput. Program. 66 2 (2007) 125\u2013153.","DOI":"10.1016\/j.scico.2006.07.002"},{"key":"e_1_3_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Francisco Dur\u00e1n and Jos\u00e9 Meseguer. 2012. On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic and Logic Programming 81 (2012) 816\u2013850.","DOI":"10.1016\/j.jlap.2011.12.004"},{"key":"e_1_3_3_2_36_2","doi-asserted-by":"crossref","unstructured":"Francisco Dur\u00e1n Jos\u00e9 Meseguer and Camilo Rocha. 2020. Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebraic Methods Program. 111 (2020) 100513.","DOI":"10.1016\/j.jlamp.2019.100513"},{"key":"e_1_3_3_2_37_2","doi-asserted-by":"crossref","unstructured":"Jonas Eckhardt Tobias M\u00fchlbauer Jos\u00e9 Meseguer and Martin Wirsing. 2015. Semantics distributed implementation and formal analysis of KLAIM models in Maude. Sci. Comput. Program. 99 (2015) 24\u201374.","DOI":"10.1016\/j.scico.2014.10.001"},{"key":"e_1_3_3_2_38_2","doi-asserted-by":"crossref","unstructured":"Steven Eker Narciso Mart\u00ed-Oliet Jos\u00e9 Meseguer Rub\u00e9n Rubio and Alberto Verdejo. 2023. The Maude strategy language. J. Log. Algebraic Methods Program. 134 (2023) 100887.","DOI":"10.1016\/j.jlamp.2023.100887"},{"key":"e_1_3_3_2_39_2","volume-title":"Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications","author":"Eker Steven","year":"2002","unstructured":"Steven Eker, Jos\u00e9 Meseguer, and Ambarish Sridharanarayanan. 2002. The Maude LTL model checker. In Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, F.\u00a0Gadducci and U.\u00a0Montanari (Eds.). ENTCS, Elsevier."},{"key":"e_1_3_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Maribel Fern\u00e1ndez and Murdoch\u00a0J. Gabbay. 2007. Nominal Rewriting. Inf. Comput. 205 6 (June 2007) 917\u2013965.","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"e_1_3_3_2_41_2","volume-title":"LFMTP","author":"Fern\u00e1ndez Maribel","year":"2010","unstructured":"Maribel Fern\u00e1ndez and Murdoch\u00a0J. Gabbay. 2010. Closed Nominal Rewriting and Efficiently Computable Nominal Algebra Equality. In LFMTP."},{"key":"e_1_3_3_2_42_2","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/1013963.1013978","volume-title":"PPDP","author":"Fern\u00e1ndez Maribel","year":"2004","unstructured":"Maribel Fern\u00e1ndez, Murdoch\u00a0J. Gabbay, and Ian Mackie. 2004. Nominal Rewriting Systems. In PPDP. ACM Press, 108\u2013119."},{"key":"e_1_3_3_2_43_2","first-page":"193","volume-title":"Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS 1999)","author":"Fiore Marcelo\u00a0P.","year":"1999","unstructured":"Marcelo\u00a0P. Fiore, Gordon\u00a0D. Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS 1999). IEEE Computer Society Press, 193\u2013202."},{"key":"e_1_3_3_2_44_2","first-page":"193","volume-title":"14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999","author":"Fiore Marcelo\u00a0P.","year":"1999","unstructured":"Marcelo\u00a0P. Fiore, Gordon\u00a0D. Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999. IEEE Computer Society, 193\u2013202."},{"key":"e_1_3_3_2_45_2","doi-asserted-by":"crossref","unstructured":"Murdoch\u00a0J. Gabbay. 2011. Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic (2011).","DOI":"10.2178\/bsl\/1305810911"},{"key":"e_1_3_3_2_46_2","doi-asserted-by":"crossref","unstructured":"Murdoch\u00a0J. Gabbay and Aad Mathijssen. 2009. Nominal Universal Algebra: Equational Logic with Names and Binding. J. Log. Comput. 19 6 (Dec. 2009) 1455\u20131508.","DOI":"10.1093\/logcom\/exp033"},{"key":"e_1_3_3_2_47_2","doi-asserted-by":"crossref","unstructured":"Murdoch\u00a0J. Gabbay and Andrew\u00a0M. Pitts. 2001. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13 3\u20135 (July 2001) 341\u2013363.","DOI":"10.1007\/s001650200016"},{"key":"e_1_3_3_2_48_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1007\/978-3-642-54624-2_29","volume-title":"Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi","author":"G\u00e2in\u00e2 Daniel","year":"2014","unstructured":"Daniel G\u00e2in\u00e2, Dorel Lucanu, Kazuhiro Ogata, and Kokichi Futatsugi. 2014. On Automation of OTS\/CafeOBJ Method. In Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi(Lecture Notes in Computer Science, Vol.\u00a08373). Springer, 578\u2013602."},{"key":"e_1_3_3_2_49_2","doi-asserted-by":"crossref","unstructured":"Lorenzo Gheri and Andrei Popescu. 2020. A Formalized General Theory of Syntax with Bindings: Extended Version. J. Autom. Reason. 64 4 (2020) 641\u2013675.","DOI":"10.1007\/s10817-019-09522-2"},{"key":"e_1_3_3_2_50_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-45127-7_9","volume-title":"RTA 2001","author":"Giesl J\u00fcrgen","year":"2001","unstructured":"J\u00fcrgen Giesl and Deepak Kapur. 2001. Dependency Pairs for Equational Rewriting. In RTA 2001(Lecture Notes in Computer Science, Vol.\u00a02051). Springer, 93\u2013108."},{"key":"e_1_3_3_2_51_2","series-title":"LNCS","first-page":"356","volume-title":"Proc. Fifth Conference on Automated Deduction","volume":"87","author":"Goguen Joseph","year":"1980","unstructured":"Joseph Goguen. 1980. How to Prove Algebraic Inductive Hypotheses without Induction: with Applications to the Correctness of Data Type Representations. In Proc. Fifth Conference on Automated Deduction. LNCS, Vol.\u00a087. Springer, 356\u2013373."},{"key":"e_1_3_3_2_52_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-53162-9_27","volume-title":"Algebraic and Logic Programming, Second International Conference, Nancy, France, October 1-3, 1990, Proceedings","volume":"463","author":"Goguen Joseph","year":"1990","unstructured":"Joseph Goguen. 1990. Proving and Rewriting. In Algebraic and Logic Programming, Second International Conference, Nancy, France, October 1-3, 1990, Proceedings(Lecture Notes in Computer Science, Vol.\u00a0463). Springer, 1\u201324."},{"key":"e_1_3_3_2_53_2","doi-asserted-by":"crossref","unstructured":"Joseph Goguen and Rod Burstall. 1992. Institutions: Abstract Model Theory for Specification and Programming. J. ACM 39 1 (1992) 95\u2013146.","DOI":"10.1145\/147508.147524"},{"key":"e_1_3_3_2_54_2","doi-asserted-by":"crossref","unstructured":"Joseph Goguen and Jos\u00e9 Meseguer. 1992. Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance Overloading Exceptions and Partial Operations. Theoretical Computer Science 105 (1992) 217\u2013273.","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_3_3_2_55_2","first-page":"80","volume-title":"Current Trends in Programming Methodology","author":"Goguen J.","year":"1978","unstructured":"J. Goguen, J.\u00a0W. Thatcher, and E.\u00a0G. Wagner. 1978. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, R.\u00a0Yeh (Ed.). Prentice-Hall, 80\u2013149."},{"key":"e_1_3_3_2_56_2","unstructured":"R. Guti\u00e9rrez J. Meseguer and S. Skeirik. [n. d.]. The Maude termination assistant. In Pre-Proceedings of WRLA 2018."},{"key":"e_1_3_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"e_1_3_3_2_58_2","doi-asserted-by":"crossref","unstructured":"Robert Harper Furio Honsell and Gordon Plotkin. 1993. A framework for defining logics. JACM 40 1 (1993) 143\u2013184.","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_3_2_59_2","first-page":"275","volume-title":"ITP 2010","author":"Hendrix Joe","year":"2010","unstructured":"Joe Hendrix, Deepak Kapur, and Jos\u00e9 Meseguer. 2010. Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. In ITP 2010 , Vol.\u00a06172. Springer LNCS, 275\u2013290."},{"key":"e_1_3_3_2_60_2","unstructured":"Joseph\u00a0D. Hendrix. 2008. Decision Procedures for Equationally Based Reasoning. Ph.\u00a0D. Dissertation. University of Illinois at Urbana-Champaign. http:\/\/hdl.handle.net\/2142\/10967."},{"key":"e_1_3_3_2_61_2","doi-asserted-by":"publisher","unstructured":"G\u00e9rard\u00a0P. Huet and Jean-Marie Hullot. 1982. Proofs by Induction in Equational Theories with Constructors. J. Comput. Syst. Sci. 25 2 (1982) 239\u2013266. 10.1016\/0022-0000(82)90006-X","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"e_1_3_3_2_62_2","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchner. 1986. Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal of Computing 15 (November 1986) 1155\u20131194.","DOI":"10.1137\/0215084"},{"key":"e_1_3_3_2_63_2","doi-asserted-by":"publisher","unstructured":"Deepak Kapur and David\u00a0R. Musser. 1987. Proof by Consistency. Artif. Intell. 31 2 (1987) 125\u2013157. 10.1016\/0004-3702(87)90017-8","DOI":"10.1016\/0004-3702(87)90017-8"},{"key":"e_1_3_3_2_64_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/3-540-51081-8_138","volume-title":"Proc. RTA-89","author":"Kapur Deepak","year":"1989","unstructured":"Deepak Kapur and Hantao Zhang. 1989. An Overview of Rewrite Rule Laboratory (RRL). In Proc. RTA-89(Lecture Notes in Computer Science, Vol.\u00a0355). Springer, 559\u2013563."},{"key":"e_1_3_3_2_65_2","doi-asserted-by":"crossref","unstructured":"Jan\u00a0Willem Klop Vincent van Oostrom and Femke van Raamsdonk. 1993. Combinatory Reduction Systems: Introduction and Survey. Theor. Comput. Sci. 121 1&2 (1993) 279\u2013308.","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"e_1_3_3_2_66_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"209","volume-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)","volume":"6","author":"Levy Jordi","year":"2010","unstructured":"Jordi Levy and Mateu Villaret. 2010. An Efficient Nominal Unification Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a06). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 209\u2013226."},{"key":"e_1_3_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.5555\/208683.208700"},{"key":"e_1_3_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0464-9_1"},{"key":"e_1_3_3_2_69_2","doi-asserted-by":"crossref","unstructured":"Richard Mayr and Tobias Nipkow. 1998. Higher-order Rewrite Systems and their Confluence. Theor. Comp. Sci. 192 (1998) 3\u201329.","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"e_1_3_3_2_70_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. 1992. Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96 1 (1992) 73\u2013155.","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_3_2_71_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. 2012. Twenty years of rewriting logic. J. Algebraic and Logic Programming 81 (2012) 721\u2013781.","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_3_3_2_72_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. 2014. Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83 (2014) 3\u201334.","DOI":"10.1016\/j.scico.2013.07.004"},{"key":"e_1_3_3_2_73_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. 2017. Strict coherence of conditional rewriting modulo axioms. Theor. Comput. Sci. 672 (2017) 1\u201335.","DOI":"10.1016\/j.tcs.2016.12.026"},{"key":"e_1_3_3_2_74_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer. 2020. Generalized rewrite theories coherence completion and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020).","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"e_1_3_3_2_75_2","first-page":"459","volume-title":"Algebraic Methods in Semantics","author":"Meseguer Jos\u00e9","year":"1985","unstructured":"Jos\u00e9 Meseguer and Joseph Goguen. 1985. Initiality, Induction and Computability. In Algebraic Methods in Semantics, Maurice Nivat and John Reynolds (Eds.). Cambridge University Press, 459\u2013541."},{"key":"e_1_3_3_2_76_2","doi-asserted-by":"crossref","unstructured":"J. Meseguer and G. Ro\u015fu. 2007. The Rewriting Logic Semantics Project. Theoretical Computer Science 373 (2007) 213\u2013237.","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"e_1_3_3_2_77_2","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Fundamentals of Computation Theory, FCT 2011","author":"Meseguer Jos\u00e9","year":"2011","unstructured":"Jos\u00e9 Meseguer and Grigore Rosu. 2011. The Rewriting Logic Semantics Project: A Progress Report. In Fundamentals of Computation Theory, FCT 2011(Lecture Notes in Computer Science, Vol.\u00a06914). Springer, 1\u201337."},{"key":"e_1_3_3_2_78_2","series-title":"LNCS","first-page":"114","volume-title":"Proc. WRLA 2020","author":"Meseguer J.","year":"2020","unstructured":"J. Meseguer and S. Skeirik. 2020. Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification. In Proc. WRLA 2020(LNCS, Vol.\u00a012328). Springer, 114\u2013135."},{"key":"e_1_3_3_2_79_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-031-12441-9_10","volume-title":"Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022","author":"Meseguer Jos\u00e9","year":"2022","unstructured":"Jos\u00e9 Meseguer and Stephen Skeirik. 2022. On Ground Convergence and Completeness of Conditional Equational Program Hierarchies. In Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022, Munich, Germany, April 2-3, 2022(Lecture Notes in Computer Science, Vol.\u00a013252). Springer, 191\u2013211."},{"key":"e_1_3_3_2_80_2","volume-title":"Communicating and mobile systems: the \u03c0 -calculus","author":"Milner Robin","year":"1999","unstructured":"Robin Milner. 1999. Communicating and mobile systems: the \u03c0 -calculus. Cambridge University Press."},{"key":"e_1_3_3_2_81_2","first-page":"154","volume-title":"Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980","author":"Musser David\u00a0R.","year":"1980","unstructured":"David\u00a0R. Musser. 1980. On Proving Inductive Properties of Abstract Data Types. In Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980. ACM Press, 154\u2013162."},{"key":"e_1_3_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_3_2_83_2","doi-asserted-by":"crossref","unstructured":"Carlos Olarte Elaine Pimentel and Camilo Rocha. 2023. A rewriting logic approach to specification proof-search and meta-proofs in sequent systems. J. Log. Algebraic Methods Program. 130 (2023) 100827.","DOI":"10.1016\/j.jlamp.2022.100827"},{"key":"e_1_3_3_2_84_2","doi-asserted-by":"crossref","unstructured":"G.\u00a0E. Peterson and M.\u00a0E. Stickel. 1981. Complete Sets of Reductions for Some Equational Theories. Journal of the Association Computing Machinery 28 2 (1981) 233\u2013264.","DOI":"10.1145\/322248.322251"},{"key":"e_1_3_3_2_85_2","series-title":"LNCS","first-page":"202","volume-title":"CADE\u201916","author":"Pfenning Frank","year":"1999","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. 1999. System description: Twelf \u2014 A Meta-logical Framework for Deductive Systems. In CADE\u201916(LNCS, Vol.\u00a01632). Springer, 202\u2013206."},{"key":"e_1_3_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_3_3_2_87_2","series-title":"LNCS","first-page":"219","volume-title":"TACS","author":"Pitts Andrew\u00a0M.","year":"2001","unstructured":"Andrew\u00a0M. Pitts. 2001. Nominal Logic: A First Order Theory of Names and Binding. In TACS(LNCS, Vol.\u00a02215). Springer, 219\u2013242."},{"key":"e_1_3_3_2_88_2","doi-asserted-by":"crossref","unstructured":"Andrew\u00a0M. Pitts. 2003. Nominal Logic A First Order Theory of Names and Binding. Inf. Comput. 186 2 (2003) 165\u2013193.","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_3_2_90_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/10722010_15","volume-title":"Proceedings of the 5th international conference on the mathematics of program construction (MPC 2000)","volume":"1837","author":"Pitts Andrew\u00a0M.","year":"2000","unstructured":"Andrew\u00a0M. Pitts and Murdoch\u00a0J. Gabbay. 2000. A Metalanguage for Programming with Bound Names Modulo Renaming. In Proceedings of the 5th international conference on the mathematics of program construction (MPC 2000)(LNCS, Vol.\u00a01837). Springer, 230\u2013255."},{"key":"e_1_3_3_2_91_2","doi-asserted-by":"publisher","unstructured":"Andrei Popescu. 2024. Nominal Recursors as Epi-Recursors. Proc. ACM Program. Lang. 8 POPL Article 15 (jan 2024) 32\u00a0pages. 10.1145\/3632857","DOI":"10.1145\/3632857"},{"key":"e_1_3_3_2_92_2","unstructured":"Albert Rubio. 1994. Automated Deduction with Constrained Clauses. Ph.\u00a0D. Dissertation. Universitat Polit\u00e8cnica de Catalunya."},{"key":"e_1_3_3_2_93_2","doi-asserted-by":"crossref","unstructured":"Albert Rubio. 2002. A Fully Syntactic AC-RPO. Inf. Comput. 178 2 (2002) 515\u2013533.","DOI":"10.1006\/inco.2002.3158"},{"key":"e_1_3_3_2_94_2","doi-asserted-by":"crossref","unstructured":"T. Serbanuta G. Ro\u015fu and J. Meseguer. 2009. A Rewriting Logic Approach to Operational Semantics. Inf. Comput. 207 2 (2009) 305\u2013340.","DOI":"10.1016\/j.ic.2008.03.026"},{"key":"e_1_3_3_2_95_2","doi-asserted-by":"crossref","unstructured":"Stephen Skeirik Andrei Stefanescu and Jos\u00e9 Meseguer. 2020. A Constructor-Based Reachability Logic for Rewrite Theories. Fundam. Inform. 173 4 (2020) 315\u2013382.","DOI":"10.3233\/FI-2020-1926"},{"key":"e_1_3_3_2_96_2","doi-asserted-by":"crossref","unstructured":"M.-O. Stehr. 2000. CINNI - A Generic Calculus of Explicit Substitutions and its Application to \u03bb - \u03c2 - and \u03c0 -calculi K.\u00a0Futatsugi (Ed.). ENTCS 36 Elsevier. Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications.","DOI":"10.1016\/S1571-0661(05)80125-2"},{"key":"e_1_3_3_2_97_2","volume-title":"Petri Nets for System Engineering \u2013 A Guide to Modelling, Verification, and Applications","author":"Stehr M.-O.","year":"2000","unstructured":"M.-O. Stehr. 2000. A Rewriting Semantics for Algebraic Nets. In Petri Nets for System Engineering \u2013 A Guide to Modelling, Verification, and Applications, C.\u00a0Girault and R.\u00a0Valk (Eds.). Springer-Verlag."},{"key":"e_1_3_3_2_98_2","first-page":"334","volume-title":"Essays in Memory of Ole-Johan Dahl","author":"Stehr M.-O.","year":"2004","unstructured":"M.-O. Stehr and J. Meseguer. 2004. Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework. In Essays in Memory of Ole-Johan Dahl. Springer LNCS Vol. 2635, 334\u2013375."},{"key":"e_1_3_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2015.301"},{"key":"e_1_3_3_2_100_2","volume-title":"Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications","author":"Thati Prasanna","year":"2002","unstructured":"Prasanna Thati, Koushik Sen, and Narciso Mart\u00ed-Oliet. 2002. An Executable Specification of Asynchronous Pi-Calculus Semantics and May Testing in Maude 2.0. In Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, F.\u00a0Gadducci and U.\u00a0Montanari (Eds.). ENTCS, Elsevier."},{"key":"e_1_3_3_2_101_2","doi-asserted-by":"crossref","unstructured":"Christian Urban. 2008. Nominal Techniques in Isabelle\/HOL. J. Autom. Reason. 40 4 (May 2008) 327\u2013356.","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_3_2_102_2","doi-asserted-by":"crossref","unstructured":"Christian Urban and Cezary Kaliszyk. 2012. General Bindings and Alpha-Equivalence in Nominal Isabelle. Log. Methods Comput. Sci. 8 2 (2012).","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"e_1_3_3_2_103_2","doi-asserted-by":"crossref","unstructured":"Christian Urban Andrew\u00a0M. Pitts and Murdoch\u00a0J. Gabbay. 2004. Nominal Unification. Theor. Comp. Sci. 323 1\u20133 (2004) 473\u2013497.","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"e_1_3_3_2_104_2","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proc. First Intl. Workshop on Rewriting Logic and its Applications","author":"Viry P.","year":"1996","unstructured":"P. Viry. 1996. Input\/Output for ELAN. In Proc. First Intl. Workshop on Rewriting Logic and its Applications(Electronic Notes in Theoretical Computer Science, Vol.\u00a04), J.\u00a0Meseguer (Ed.). Elsevier. http:\/\/www.elsevier.nl\/cas\/tree\/store\/tcs\/free\/noncas\/pc\/volume4.htm."},{"key":"e_1_3_3_2_105_2","doi-asserted-by":"crossref","unstructured":"P. Viry. 2002. Equational rules for rewriting logic. Theoretical Computer Science 285 (2002) 487\u2013517. Issue 2.","DOI":"10.1016\/S0304-3975(01)00366-8"}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:51Z","timestamp":1765617591000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":104,"alternative-id":["10.1145\/3756907.3756921","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756921","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}