Matching and alpha-equivalence check for nominal terms

Nominal techniques were introduced to represent in a simple and natural way that involve binders. The syntax includes an abstraction operator and a primitive notion of name swapping. Nominal matching is matching modulo α-equality, and has applications in programming languages and theorem proving, amongst others. In this paper we describe efficient algorithms to check the validity of equations involving binders, and also to solve matching problems modulo α-equivalence, using the nominal approach.

• Type: Journal
• Year: 2010
• Where: JCSS
• Authors: Christophe Calvès, Maribel Fernández
• Keywords: JCSS 2010, Modulo α-equality, Nominal Approach, Nominal Techniques