A Formalisation of Nominal C-Matching through Unification with Protected Variables

This work adapts a formalisation in Coq of a nominal C-unification algorithm to include “protected variables” that cannot be instantiated during the unification process. By introducing protected variables we are able to reuse the C-unification algorithm to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view having this extension would be enough to adapt the C-unification algorithm for dealing with equational check as well as with C-matching problems, but the resulting algorithms would not be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification and reuse previous formalisations.