Computer Science – Logic in Computer Science
Scientific paper
2010-12-22
EPTCS 42, 2010, pp. 1-11
Computer Science
Logic in Computer Science
In Proceedings UNIF 2010, arXiv:1012.4554
Scientific paper
10.4204/EPTCS.42.1
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it clearly apart from higher-order pattern unification. The purpose of this paper is to simplify a clunky proof from the original paper on nominal unification and to give an overview over some results about nominal unification.
No associations
LandOfFree
Nominal Unification Revisited does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Nominal Unification Revisited, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Nominal Unification Revisited will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-581918