Ramana Kumar, Michael Norrish: (Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP 2010: 51-66