Skip to main content

TS

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

Download

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.