{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T02:10:02Z","timestamp":1754014202265,"version":"3.41.2"},"reference-count":45,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[2021,8]]},"DOI":"10.1016\/j.jcss.2021.01.002","type":"journal-article","created":{"date-parts":[[2021,2,4]],"date-time":"2021-02-04T16:13:27Z","timestamp":1612455207000},"page":"34-59","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Nominal syntax with atom substitutions"],"prefix":"10.1016","volume":"119","author":[{"given":"Jes\u00fas","family":"Dom\u00ednguez","sequence":"first","affiliation":[]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.jcss.2021.01.002_br0010","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s001650200016","article-title":"A new approach to abstract syntax with variable binding","volume":"13","author":"Gabbay","year":"2001","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.jcss.2021.01.002_br0020","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","article-title":"Nominal unification","volume":"323","author":"Urban","year":"2004","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0030","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1016\/j.tcs.2008.05.012","article-title":"A polynomial nominal unification algorithm","volume":"403","author":"Calv\u00e8s","year":"2008","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0040","series-title":"RTA-2010","first-page":"209","article-title":"An efficient nominal unification algorithm","author":"Levy","year":"2010"},{"key":"10.1016\/j.jcss.2021.01.002_br0050","series-title":"LOPSTR 2010","first-page":"234","article-title":"The first-order nominal link","author":"Calv\u00e8s","year":"2010"},{"key":"10.1016\/j.jcss.2021.01.002_br0060","article-title":"Matching and alpha-equivalence check for nominal terms","author":"Calv\u00e8s","year":"2009","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0070","series-title":"Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming","first-page":"108","article-title":"Nominal rewriting systems","author":"Fern\u00e1ndez","year":"2004"},{"key":"10.1016\/j.jcss.2021.01.002_br0080","doi-asserted-by":"crossref","first-page":"917","DOI":"10.1016\/j.ic.2006.12.002","article-title":"Nominal rewriting","volume":"205","author":"Fern\u00e1ndez","year":"2007","journal-title":"Inf. Comput."},{"key":"10.1016\/j.jcss.2021.01.002_br0090","series-title":"26th Int. Conference on Rewriting Techniques and Applications","first-page":"301","article-title":"Confluence of orthogonal nominal rewriting systems revisited","author":"Suzuki","year":"2015"},{"key":"10.1016\/j.jcss.2021.01.002_br0100","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/j.entcs.2007.02.009","article-title":"Nominal equational logic","volume":"172","author":"Clouston","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0110","series-title":"Logic Programming, Proceedings of the 24th International Conference, ICLP 2008, Udine, Italy, December 9-13","first-page":"238","article-title":"alpha-leanTAP: a declarative theorem prover for first-order classical logic","author":"Near","year":"2008"},{"key":"10.1016\/j.jcss.2021.01.002_br0120","series-title":"Proceedings 5th Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice","first-page":"37","article-title":"Closed nominal rewriting and efficiently computable nominal algebra equality","author":"Fern\u00e1ndez","year":"2010"},{"key":"10.1016\/j.jcss.2021.01.002_br0130","doi-asserted-by":"crossref","DOI":"10.1093\/logcom\/exp033","article-title":"Nominal universal algebra: equational logic with names and binding","author":"Gabbay","year":"2009","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.jcss.2021.01.002_br0140","doi-asserted-by":"crossref","first-page":"769","DOI":"10.1093\/jigpal\/jzq006","article-title":"Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques","volume":"18","author":"Dowek","year":"2010","journal-title":"IGPL-10"},{"key":"10.1016\/j.jcss.2021.01.002_br0150","series-title":"Logic Programming","first-page":"269","article-title":"\u03b1Prolog: a logic programming language with names, binding and \u03b1-equivalence","author":"Cheney","year":"2004"},{"key":"10.1016\/j.jcss.2021.01.002_br0160","series-title":"Proceedings of the 2007 Workshop on Scheme and Functional Programming","first-page":"79","article-title":"\u03b1Kanren: a fresh name in nominal logic programming","author":"Byrd","year":"2007"},{"key":"10.1016\/j.jcss.2021.01.002_br0170","series-title":"MPC 2000","first-page":"230","article-title":"A metalanguage for programming with bound names modulo renaming","author":"Pitts","year":"2000"},{"doi-asserted-by":"crossref","unstructured":"M.R. Shinwell, A.M. Pitts, M.J. Gabbay, FreshML: programming with binders made simple, 2003, pp. 263\u2013274, SIGPLAN-03 38.","key":"10.1016\/j.jcss.2021.01.002_br0180","DOI":"10.1145\/944746.944729"},{"key":"10.1016\/j.jcss.2021.01.002_br0190","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/j.entcs.2005.11.039","article-title":"An overview of C\u03b1ML","volume":"148","author":"Pottier","year":"2006","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0200","series-title":"Proceedings of the 22nd IEEE Symposium on Logic in Computer Science","first-page":"356","article-title":"Static name control for FreshML","author":"Pottier","year":"2007"},{"key":"10.1016\/j.jcss.2021.01.002_br0210","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s00165-007-0056-1","article-title":"Capture-avoiding substitution as a nominal algebra","volume":"20","author":"Gabbay","year":"2008","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.jcss.2021.01.002_br0220","series-title":"TLCA-15","first-page":"180","article-title":"Dependent types for nominal terms with atom substitutions","volume":"vol. 38","author":"Fairweather","year":"2015"},{"key":"10.1016\/j.jcss.2021.01.002_br0230","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0240","series-title":"Fundamentals of Computation Theory - Proceedings of the 22nd International Symposium","first-page":"64","article-title":"Nominal syntax with atom substitutions: matching, unification, rewriting","author":"Dom\u00ednguez","year":"2019"},{"key":"10.1016\/j.jcss.2021.01.002_br0250","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","article-title":"Nominal logic, a first order theory of names and binding","volume":"186","author":"Pitts","year":"2003","journal-title":"Inf. Comput."},{"year":"1998","author":"Baader","series-title":"Term Rewriting and All That","key":"10.1016\/j.jcss.2021.01.002_br0260"},{"key":"10.1016\/j.jcss.2021.01.002_br0270","series-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming","first-page":"47","article-title":"Nominal rewriting with name generation: abstraction vs. locality","author":"Fern\u00e1ndez","year":"2005"},{"key":"10.1016\/j.jcss.2021.01.002_br0280","series-title":"Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications","first-page":"39","article-title":"Checking overlaps of nominal rewriting rules","volume":"vol. 323","author":"Ayala-Rinc\u00f3n","year":"2015"},{"key":"10.1016\/j.jcss.2021.01.002_br0290","series-title":"Handbook of Theoretical Computer Science, volume B","first-page":"243","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"key":"10.1016\/j.jcss.2021.01.002_br0300","first-page":"279","article-title":"Enumerable sets are Diophantine","volume":"191","author":"Matiyasevich","year":"1970","journal-title":"Sov. Math. Dokl."},{"key":"10.1016\/j.jcss.2021.01.002_br0310","series-title":"Computer Science Logic, Proceedings of the 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt G\u00f6del Colloquium","first-page":"513","article-title":"Nominal unification","author":"Urban","year":"2003"},{"key":"10.1016\/j.jcss.2021.01.002_br0320","article-title":"From nominal to higher-order rewriting and back again","volume":"11","author":"Dom\u00ednguez","year":"2015","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0330","series-title":"WoLLIC 2008","first-page":"111","article-title":"Nominal matching and alpha-equivalence","author":"Calv\u00e8s","year":"2008"},{"key":"10.1016\/j.jcss.2021.01.002_br0340","series-title":"RTA-13","first-page":"143","article-title":"Unifying nominal unification","volume":"vol. 21","author":"Calv\u00e8s","year":"2013"},{"key":"10.1016\/j.jcss.2021.01.002_br0350","series-title":"IITP 2010","first-page":"51","article-title":"(nominal) unification by recursive descent with triangular substitutions","author":"Kumar","year":"2010"},{"key":"10.1016\/j.jcss.2021.01.002_br0360","series-title":"Automata, Languages and Programming: Proceedings of the 31st International Colloquium","first-page":"332","article-title":"The complexity of equivariant unification","volume":"vol. 3142","author":"Cheney","year":"2004"},{"key":"10.1016\/j.jcss.2021.01.002_br0370","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2007.01.017","article-title":"Hierarchical nominal terms and their theory of rewriting","volume":"174","author":"Gabbay","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"year":"1978","author":"Huet","series-title":"On the Uniform Halting Problem for Term Rewriting Systems","key":"10.1016\/j.jcss.2021.01.002_br0380"},{"key":"10.1016\/j.jcss.2021.01.002_br0390","series-title":"Mathematical Foundations of Computer Science, Proceedings of the 16th International Symposium","first-page":"151","article-title":"A second-order pattern matching algorithm for the cube of typed lambda-calculi","author":"Dowek","year":"1991"},{"key":"10.1016\/j.jcss.2021.01.002_br0400","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(94)90083-3","article-title":"Third order matching is decidable","volume":"69","author":"Dowek","year":"1994","journal-title":"Ann. Pure Appl. Log."},{"key":"10.1016\/j.jcss.2021.01.002_br0410","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129500003108","article-title":"Decidability of fourth-order matching","volume":"10","author":"Padovani","year":"2000","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/j.jcss.2021.01.002_br0420","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1006\/inco.2000.2877","article-title":"On the undecidability of second-order unification","volume":"159","author":"Levy","year":"2000","journal-title":"Inf. Comput."},{"key":"10.1016\/j.jcss.2021.01.002_br0430","series-title":"UNIF-05","first-page":"104","article-title":"Relating nominal and higher-order pattern unification","author":"Cheney","year":"2005"},{"key":"10.1016\/j.jcss.2021.01.002_br0440","doi-asserted-by":"crossref","DOI":"10.1145\/2159531.2159532","article-title":"Nominal unification from a higher-order perspective","volume":"13","author":"Levy","year":"2012","journal-title":"ACM Trans. Comput. Log."},{"key":"10.1016\/j.jcss.2021.01.002_br0450","series-title":"LFMTP-10","first-page":"5","article-title":"Explicit substitutions for contextual type theory","author":"Abel","year":"2010"}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000021000106?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000021000106?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T01:34:38Z","timestamp":1754012078000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000021000106"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":45,"alternative-id":["S0022000021000106"],"URL":"https:\/\/doi.org\/10.1016\/j.jcss.2021.01.002","relation":{},"ISSN":["0022-0000"],"issn-type":[{"type":"print","value":"0022-0000"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Nominal syntax with atom substitutions","name":"articletitle","label":"Article Title"},{"value":"Journal of Computer and System Sciences","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jcss.2021.01.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2021 Elsevier Inc.","name":"copyright","label":"Copyright"}]}}