(nominal) unification by recursive descent with triangular substitutions
Authors
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, month = jul, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/3724.pdf}, booktitle = {International Conference on Interactive Theorem Proving}, slides = {http://ts.data61.csiro.au/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} }