Matching and alpha-equivalence check for nominal terms
Nominal terms generalise first-order terms by including abstraction and name swapping constructs, alpha-equivalence can be easily axiomatised using name swappings and a freshness relation, which makes the nominal approach well adapted to the specification of systems that involve binders. Nominal matching is matching modulo alpha-equivalence and has applications in programming languages, rewriting, and theorem proving. In this paper, we describe efficient algorithms to check the validity of equations involving binders and to solve matching problems modulo alpha-equivalence, using the nominal approach. (C) 2009 Elsevier Inc. All rights reserved.
matching alpha-equivalence nominal terms binders