Sciweavers

JCSS
2010

Matching and alpha-equivalence check for nominal terms

13 years 27 days ago
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.
Christophe Calvès, Maribel Fernández
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JCSS
Authors Christophe Calvès, Maribel Fernández
Comments (0)