(Nominal) Unification by Recursive Descent with Triangular Substitutions

Author:

Kumar, Ramana; Norrish, Michael

Date of Publication:

2010-07-11

Publication Type:

Conference Material

Conference Name:

International Conference on Interactive Theorem Proving

Conference Location:

Edinburgh, United Kingdom

Pages:

51-66

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.

URL:

http://www.floc-conference.org/ITP-home.html

Identifier:

nicta:3724

Attribution Statement:

Kumar, Ramana; Norrish, Michael. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In: International Conference on Interactive Theorem Proving; Edinburgh, United Kingdom. 2010-07-11. 51-66.