S. Berghofer and C. Urban, A Head-to-Head Comparison of de Bruijn Indices and Names, Electronic Notes in Theoretical Computer Science, vol.174, issue.5, pp.53-67, 2007.
DOI : 10.1016/j.entcs.2007.01.018

J. Cheney, Nominal logic and abstract syntax SIGACT News (logic column 14, CP07] Ranald A. Clouston and Andrew M. Pitts. Nominal equational logic, pp.47-69223, 2005.

I. Cheney and C. Urban, System description: Alpha-Prolog, a fresh approach to logic programming modulo alpha-equivalence Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae, vol.5, issue.34, pp.381-392, 1972.

G. Dowek, M. Fernández, and M. J. Gabbay, Higher-order unification and matching Nominal rewriting with name generation: abstraction vs. locality, Handbook of automated reasoning Proc, pp.1009-1062, 2001.

M. Fernández and M. J. Gabbay, Nominal rewriting. Information and Computation, pp.917-965, 2007.

J. Murdoch and . Gabbay, Nominal algebra and the HSP theorem, Journal of Logic and Computation, 2008.

J. Murdoch, S. Gabbay, and . Lengrand, The lambda-context calculus, GM07] Murdoch J. Gabbay and Aad Mathijssen, pp.19-35, 2008.

J. Murdoch, A. M. Gabbay, and . Pitts, A new approach to abstract syntax involving binders, 14th Annual Symposium on Logic in Computer ScienceGP01] Murdoch J. Gabbay and A. M. Pitts, pp.214-224, 1999.

M. Hamana, A Logic Programming Language Based on Binding Algebras, TACS'01, pp.243-262
DOI : 10.1007/3-540-45500-0_12

J. Levy and M. Villaret, Nominal unification from a higher-order perspective, Proceedings of RTA'08, 2008.

A. Mathijssen, . Calculi, . Reasoning, and . Binding, [Mil91] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification On theories with a combinatorial definition of equivalence, Journal of Logic and Computation Annals of Mathematics, vol.1, issue.432, pp.497-536223, 1942.

P. Nickolas and P. J. Robinson, The Qu-Prolog unification algorithm: formalisation and correctness, Theoretical Computer Science, vol.169, issue.1, pp.81-112, 1996.
DOI : 10.1016/S0304-3975(96)00115-6
URL : http://doi.org/10.1016/s0304-3975(96)00115-6

A. M. Pitts, Equivariant Syntax and Semantics, Proceedings of ICALP'02, pp.32-36, 2002.
DOI : 10.1007/3-540-45465-9_3