(Nominal) Unification by Recursive Descent with Triangular Substitutions

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]

@inproceedings{KumarN10,
  title = {(Nominal) Unification by Recursive Descent with Triangular Substitutions},
  author = {Ramana Kumar and Michael Norrish},
  year = {2010},
  doi = {10.1007/978-3-642-14052-5_6},
  url = {http://dx.doi.org/10.1007/978-3-642-14052-5_6},
  researchr = {https://researchr.org/publication/KumarN10},
  cites = {0},
  citedby = {0},
  pages = {51-66},
  booktitle = {Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  editor = {Matt Kaufmann and Lawrence C. Paulson},
  volume = {6172},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  isbn = {978-3-642-14051-8},
}