C. Calvès, Complexity and Implementation of Nominal Algorithms King's College of London, 2010.

C. Calvès and M. Fernández, The First-Order Nominal Link, Lecture Notes in Computer Science, vol.323, issue.1, pp.234-248, 2010.
DOI : 10.1016/j.tcs.2004.06.016

C. Calvès and M. Fernández, Matching and alpha-equivalence check for nominal terms, Journal of Computer and System Sciences, vol.76, issue.5, pp.283-301, 2010.
DOI : 10.1016/j.jcss.2009.10.003

. Cheney, Relating nominal and higher-order pattern unification, Proceedings of the 19th International Workshop on Unification (UNIF 2005), pp.104-119, 2005.

. Cheney, Equivariant Unification, Journal of Automated Reasoning, vol.323, issue.1???3, pp.267-300, 2010.
DOI : 10.1007/s10817-009-9164-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.2544

G. Dowek, M. J. Gabbay, and D. P. Mulligan, Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques, Logic Journal of IGPL, vol.18, issue.6, pp.769-822, 2010.
DOI : 10.1093/jigpal/jzq006
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.185.3105

M. Gabbay and A. M. Pitts, A new approach to abstract syntax with variable binding. Formal Asp, Comput, vol.13, issue.3-5, pp.341-363, 2002.

L. P. Simon and . Jones, The Implementation of Functional Programming Languages, 1987.

J. Levy and M. Villaret, Nominal Unification from a Higher-Order Perspective, Lecture Notes in Computer Science, vol.5117, pp.246-260, 2008.
DOI : 10.1007/978-3-540-70590-1_17

J. Levy and M. Villaret, An efficient nominal unification algorithm, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.209-226, 2010.

A. M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, vol.186, issue.2, pp.165-193, 2003.
DOI : 10.1016/S0890-5401(03)00138-X

Z. Qian, Linear unification of higher-order patterns, Lecture Notes in Computer Science, vol.668, pp.391-405, 1993.
DOI : 10.1007/3-540-56610-4_78

A. M. 13-christian-urban, M. Pitts, and . Gabbay, Nominal unification, Theoretical Computer Science, vol.323, issue.1-3, pp.473-497, 2004.
DOI : 10.1016/j.tcs.2004.06.016