Unification is also at the core of type checking algorithms in the tradition of Milner's, and a limited form - pattern matching - is available to the user in languages of the ML and Haskell family.
Writing a pattern matcher or a an unifier in Common Lisp is easy, as long as we limit ourselves to manipulate only ATOMs and CONSes.
Alas, it would be much nicer if we could manipulate arbitrary Common Lisp objects as the ML programmer can with arbitrary ML objects.
The library presented here is the first one (to the best of the author's knowledge) that is capable of manipulating arbitrary Common Lisp objects.
To reach the project page, click this link to CL Unification
Pattern matching algorithm