Alpha-Prolog is a prototype logic programming language with a built-in notion of binders and unification modulo alpha-equivalence. It is based on a mild extension of first-order Horn formulae: instead of the usual first-order terms and first-order unification, Alpha-Prolog uses nominal terms and nominal unification introduced in . In this paper, we give three examples that demonstrate the advantages of Alpha-Prolog and describe our current implementation.
|Title of host publication||Proceedings of the 17th International Workshop on Unification cheney|
|Publication status||Published - 2003|