The University of New South Wales

(nominal) unification by recursive descent with triangular substitutions

Authors

Ramana Kumar and Michael Norrish

Australian National University

NICTA

Abstract

We mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other for nominal terms (terms including alpha-equivalent binding structure). Both algorithms work with triangular substitutions in accumulator-passing style: taking a substitution as input, and returning an extension of that substitution on success.

BibTeX Entry

  @inproceedings{Kumar_Norrish_10,
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3724.pdf},
    booktitle        = {International Conference on Interactive Theorem Proving},
    slides           = {https://trustworthy.systems/publications/nicta_slides/3724.pdf},
    author           = {Kumar, Ramana and Norrish, Michael},
    year             = {2010},
    pages            = {51--66},
    title            = {(Nominal) Unification by Recursive Descent with Triangular Substitutions},
    address          = {Edinburgh, United Kingdom}
  }

Download