D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

J. Cheney, A Simpler Proof Theory for Nominal Logic, 8th International Conference on the Foundations of Software Science and Computational Structures (FOSSACS), pp.379-394, 2005.
DOI : 10.1007/978-3-540-31982-5_24

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

J. Cheney, Equivariant unification, Journal of Automated Reasoning, 2009.
DOI : 10.1007/s10817-009-9164-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.2544

J. Cheney and C. Urban, Alpha-prolog: A logic programming language with names, binding, and alpha-equivalence, Logic Programming, 20th International Conference, pp.269-283, 2004.

J. Cheney and C. Urban, Nominal logic programming, ACM Transactions on Programming Languages and Systems, vol.30, issue.5, pp.1-47, 2008.
DOI : 10.1145/1387673.1387675
URL : http://arxiv.org/abs/cs/0609062

M. J. Gabbay and J. Cheney, A sequent calculus for nominal logic, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.139-148, 2004.
DOI : 10.1109/LICS.2004.1319608

A. Gacek, The Abella Interactive Theorem Prover (System Description), Fourth International Joint Conference on Automated Reasoning, pp.154-161, 2008.
DOI : 10.1007/978-3-540-71070-7_13

A. Gacek, D. Miller, and G. Nadathur, Reasoning in Abella about Structural Operational Semantics Specifications, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice number 228 in Electronic Notes in Theoretical Computer Science, pp.85-100, 2008.
DOI : 10.1016/j.entcs.2008.12.118

A. Gacek, D. Miller, and G. Nadathur, Combining Generic Judgments with Recursive Definitions, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.33-44, 2008.
DOI : 10.1109/LICS.2008.33

R. Harper and D. R. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.613-673, 2007.
DOI : 10.1006/inco.2001.2951

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

D. Miller and G. Nadathur, A logic programming approach to manipulating formulas and programs, IEEE Symposium on Logic Programming, pp.379-388, 1987.

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic, vol.6, issue.4, pp.749-783, 2005.
DOI : 10.1145/1094622.1094628

]. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

G. Nadathur and D. Miller, An Overview of ?Prolog, Fifth International Logic Programming Conference, pp.810-827, 1988.

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.

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

A. Tiu, A Logic for Reasoning about Generic Judgments, Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006.
DOI : 10.1016/j.entcs.2007.01.016

C. Urban, Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.323, issue.1???2, pp.327-356, 2008.
DOI : 10.1007/s10817-008-9097-2

C. Urban and J. Cheney, Avoiding Equivariance in Alpha-Prolog, Typed Lambda Calculi and Applications, Proceedings, pp.401-416, 2005.
DOI : 10.1007/11417170_29

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

R. Virga, Higher-order Rewriting with Dependent Types, 1999.