(Nominal) Unification by Recursive Descent with Triangular Substitutions

Using HOL4, 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 -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.

• Type: Journal
• Year: 2010
• Where: ITP
• Authors: Ramana Kumar, Michael Norrish
• Keywords: -equivalent Binding Structure, ITP 2010, Mathematics, Recursive Descent Style, Unification Algorithms