Ramana Kumar, Michael Norrish. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In Matt Kaufmann, Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Volume 6172 of Lecture Notes in Computer Science, pages 51-66, Springer, 2010. [doi]
Abstract is missing.