{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T14:19:48Z","timestamp":1772633988906,"version":"3.50.1"},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2021,5,7]],"date-time":"2021-05-07T00:00:00Z","timestamp":1620345600000},"content-version":"unspecified","delay-in-days":67,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This work extends a rule-based specification of nominal C-unification formalised in Coq to include \u2018protected variables\u2019 that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-unification simplification rules to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view, this extension is sufficient to obtain a generalised C-unification procedure; however, it cannot be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification of the inference rules and reuse previous formalisations. We also generalise a functional recursive nominal C-unification algorithm specified in PVS with protected variables, effectively adapting this algorithm to the tasks of nominal C-matching and nominal equality check. The PVS formalisation is applied to test the correctness of a Python manual implementation of the algorithm.<\/jats:p>","DOI":"10.1017\/s0960129521000050","type":"journal-article","created":{"date-parts":[[2021,5,7]],"date-time":"2021-05-07T09:02:02Z","timestamp":1620378122000},"page":"286-311","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":13,"title":["Formalising nominal C-unification generalised with protected variables"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0089-3905","authenticated-orcid":false,"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Washington","family":"de Carvalho-Segundo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel Ferreira","family":"Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1959-8730","authenticated-orcid":false,"given":"Daniele","family":"Nantes-Sobrinho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2021,5,7]]},"reference":[{"key":"S0960129521000050_ref12","unstructured":"Calv\u00e8s, C. F. (2010). Complexity and Implementation of Nominal Algorithms. Phd thesis, King\u2019s College London."},{"key":"S0960129521000050_ref2","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-319-94460-9_14","article-title":"Nominal C-unification","volume":"10855","author":"Ayala-Rinc\u00f3n","year":"2018","journal-title":"Post-proceedings of the 27th International Symposium Logic-based Program Synthesis and Transformation (LOPSTR 2017)"},{"key":"S0960129521000050_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"S0960129521000050_ref23","unstructured":"Mu\u00f1oz, C. and Butler, R. (2003). Rapid prototyping in PVS. Technical Report NASA\/CR-2003-212418, NIA-2003-03, NASA Langley Research Center (NIA)."},{"key":"S0960129521000050_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.02.020"},{"key":"S0960129521000050_ref24","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"Pitts","year":"2013"},{"key":"S0960129521000050_ref25","first-page":"328","article-title":"Nominal unification of higher order expressions with recursive let","volume":"10184","author":"Schmidt-Schau\u00df","year":"2017","journal-title":"Post-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)"},{"key":"S0960129521000050_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BF02328451"},{"key":"S0960129521000050_ref6","unstructured":"Ayala-Rinc\u00f3n, M. , Fern\u00e1ndez, M. and Nantes-Sobrinho, D. (2018b). Fixed point constraints for nominal equational unification. In: Proceedings of the 3rd International Conference Formal Structures for Computation and Deduction (FSCD), LIPIcs, vol. 108, 7:1\u20137:16."},{"key":"S0960129521000050_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"S0960129521000050_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2009.10.003"},{"key":"S0960129521000050_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"S0960129521000050_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245463"},{"key":"S0960129521000050_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80012-4"},{"key":"S0960129521000050_ref7","first-page":"57","article-title":"Completeness in PVS of a nominal unification algorithm","volume":"323","author":"Ayala-Rinc\u00f3n","year":"2016","journal-title":"ENTCS"},{"key":"S0960129521000050_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80004-4"},{"key":"S0960129521000050_ref4","doi-asserted-by":"crossref","unstructured":"Ayala-Rinc\u00f3n, M. , de Carvalho-Segundo, W. , Fern\u00e1ndez, M. and Nantes-Sobrinho, D. (2019b). A formalisation of nominal C-matching through unification with protected variables. ENTCS 344\u00a047\u201365.","DOI":"10.1016\/j.entcs.2019.07.004"},{"key":"S0960129521000050_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20551-4_15"},{"key":"S0960129521000050_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_5"},{"key":"S0960129521000050_ref26","first-page":"531","article-title":"Matching under commutativity","volume":"72","author":"Siekmann","year":"1979","journal-title":"Proceedings of the International Symposium on Symbolic and Algebraic Manipulation (EUROSAM)"},{"key":"S0960129521000050_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/36330.36332"},{"key":"S0960129521000050_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_8"},{"key":"S0960129521000050_ref10","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0009"},{"key":"S0960129521000050_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_12"},{"key":"S0960129521000050_ref5","unstructured":"Ayala-Rinc\u00f3n, M. , Fern\u00e1ndez, M. and Nantes-Sobrinho., D . (2016a). Nominal narrowing. In: Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD), LIPIcs, vol. 52, 11:1\u201311:17."},{"key":"S0960129521000050_ref22","first-page":"209","article-title":"An efficient nominal unification algorithm","volume":"6","author":"Levy","year":"2010","journal-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA)"},{"key":"S0960129521000050_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90108-6"},{"key":"S0960129521000050_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16780-3_113"},{"key":"S0960129521000050_ref28","first-page":"1","article-title":"Nominal unification revisited","volume":"42","author":"Urban","year":"2010","journal-title":"Proceedings of the 24th International Workshop on Unification (UNIF)"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000050","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,26]],"date-time":"2022-12-26T15:53:53Z","timestamp":1672070033000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000050\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["S0960129521000050"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000050","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}