Implementations

M. Lakin. αML, a functional-logic programming language with special features for prototyping inductive definitions involving binding.

C. Calves. HNT, a Haskell Nominal Toolkit.

C. Calves, M. Fernandez. Nominal Matcher and Alpha-Equivalence Checker.
Paper (WOLLIC 2008) pdf
Software: tar file, version 0.2.3
OCAML bytecode, version 0.2.3
Executable (under Linux): ltnm-0.2.3.static

C. Calves, M. Fernandez. Implementing Nominal Unification.
Paper (TERMGRAPH'06) pdf
Software: tar file