Trustworthy Systems

(nominal) unification by recursive descent with triangular substitutions


Ramana Kumar and Michael Norrish

Australian National University



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

    address          = {Edinburgh, United Kingdom},
    author           = {Kumar, Ramana and Norrish, Michael},
    booktitle        = {International Conference on Interactive Theorem Proving},
    month            = jul,
    pages            = {51--66},
    paperurl         = {},
    slides           = {},
    title            = {(Nominal) Unification by Recursive Descent with Triangular Substitutions},
    year             = {2010}