The University of New South Wales

(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

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