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