[clarification needed] Consequently, the native notion of equality between two nominal terms is alpha-equivalence (equivalence up to a permutative renaming of bound names).
Nominal term embeddings may be seen as alternatives to de Bruijn encodings and higher-order abstract syntax, where the latter uses the simply typed lambda calculus as a metalanguage.
Many interesting calculi, logics and programming languages that are commonly seen in computer science feature name binding constructs.
For instance, the universal quantifier from first-order logic, the lambda-binder from the lambda-calculus, and the pi-binder from the pi-calculus are all examples of name-binding constructs.
They possess an efficiently decidable unification procedure, and as a result, have been widely implemented, notably in the logic programming language lambdaProlog.