I did my PhD on the complexity and implementation of nominal algorithms under the direction of Maribel Fernández. I successfully defended my thesis the 22nd February 2010.
My thesis is available here.
The code of the framework developed in the thesis is available here. It includes efficient unification, matching and alpha-equivalence algorithm and building blocks to build easily algorithms manipulating nominal terms.
A O'Caml implementation of the Quadratic Nominal Unification algorithm is available here.
An old and deprecated version of the Haskell framework is available at here.