Trustworthy Systems

(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,
    address          = {Edinburgh, UK},
    author           = {Kumar, Ramana and Norrish, Michael},
    booktitle        = {International Conference on Interactive Theorem Proving},
    month            = jul,
    pages            = {51--66},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3724.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/3724.pdf},
    title            = {(Nominal) Unification by Recursive Descent with Triangular Substitutions},
    year             = {2010}
  }

Download