Skip to main content

(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

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


Served by Apache on Linux on seL4.