H. Barendregt, The Lambda Calculus: its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, 1984.

J. Cheney, Relating Nominal and Higher-Order Pattern Unification, Proceedings of the 19th International Workshop on Unification, pp.104-119, 2005.

J. Cheney and C. Urban, ??Prolog: A Logic Programming Language with Names, Binding and ??-Equivalence, Proceedings of the 20th International Conference on Logic Programming, pp.269-283, 2004.
DOI : 10.1007/978-3-540-27775-0_19

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing, vol.13, issue.3-5, pp.341-363, 2002.
DOI : 10.1007/s001650200016

J. Levy and M. Villaret, Nominal Unification from a Higher-Order Perspective, Proceedings of Rewriting Techniques and Applications, pp.246-260, 2008.
DOI : 10.1145/2159531.2159532
URL : http://arxiv.org/pdf/1005.3731

A. Martelli and U. Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, vol.4, issue.2, pp.258-282, 1982.
DOI : 10.1145/357162.357169

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

F. Pfenning and C. Elliott, Higher-Order Abstract Syntax, Proceedings of the ACM SIGPLAN conference on Programming language design and implementation, pp.199-208, 1988.

X. Qi, An Implementation of the Language Lambda Prolog Organized around Higher-Order Pattern Unification, 2009.

K. Ueda, Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting, Proceedings of Rewriting Techniques and Applications, pp.392-408, 2008.
DOI : 10.1007/978-3-540-70590-1_27

K. Ueda and S. Ogawa, HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model, KI - K??nstliche Intelligenz, vol.410, issue.46, pp.27-36, 2012.
DOI : 10.1007/978-3-642-03466-4_24

C. Urban, A. M. Pitts, and M. J. , Nominal unification, Theoretical Computer Science, vol.323, issue.1-3, pp.473-497, 2004.
DOI : 10.1016/j.tcs.2004.06.016
URL : https://doi.org/10.1016/j.tcs.2004.06.016

C. Urban, Nominal Unification Revisited, Proceedings of UNIF 2010, pp.1-11, 2010.
DOI : 10.4204/EPTCS.42.1
URL : http://www4.in.tum.de/%7Eurbanc/Publications/univ-10.pdf

A. Yasen and K. Ueda, Hypergraph Representation of Lambda-Terms, 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE)
DOI : 10.1109/TASE.2016.25

A. Yasen and K. Ueda, Name Binding is Easy with Hypergraphs. sub- mitted

Z. Qian, Linear unification of higher-order patterns, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, pp.391-405, 1993.
DOI : 10.1007/3-540-56610-4_78

I. Mackie, Efficient ??-Evaluation with Interaction Nets, Proceedings of Rewriting Techniques and Applications, pp.155-169, 2004.
DOI : 10.1007/978-3-540-25979-4_11