ABSTRACT. We present a nominal unification algorithm that runs in O(n × G(n)) time, where G is the functional inverse of Ackermann’s function. Nominal unification generates a set of variable assignments, if there exists one, that makes terms involving binding operations α-equivalent. We preserve names while using special representations of de Bruijn numbers. Operations on name handling, i.e., deciding the α-equivalence of two names and inferring a name that α-equals to a given one, are in constant time. To reduce an arbitrary unification problem to such name handlings, we preprocess the unification terms with the idea of Martelli-Montanari.