B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich, Engineering Formal Metatheory, Proc. of the 35rd Symposium on Principles of Programming Languages (POPL), pp.3-15, 2008.
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948

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

S. Berghofer and C. Urban, A Head-to-Head Comparison of de Bruijn Indices and Names, Proc. of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), ENTCS, pp.46-59, 2006.
DOI : 10.1016/j.entcs.2007.01.018

S. Berghofer and C. Urban, Nominal Inversion Principles, Proc. of the 21th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp.71-85, 2008.
DOI : 10.1007/11532231_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.119.7125

K. Crary, Advanced Topics in Types and Programming Languages, chapter on Logical Relations and a Case Study in Equivalence Checking, pp.139-160, 2005.

H. B. Curry and R. Feys, Combinatory Logic, volume 1 of Studies in Logic and the Foundations of Mathematics, 1958.

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.645.5233

J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, 1986.

J. Mckinna and R. Pollack, Some Type Theory and Lambda Calculus Formalised, Journal of Automated Reasoning, vol.23, pp.1-4, 1999.

T. Nipkow and L. C. Paulson, Proof Pearl: Defining Functions over Finite Sets, LNCS, vol.3603, pp.385-396, 2005.
DOI : 10.1007/11541868_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.9058

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.
DOI : 10.1007/3-540-45949-9

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. M. Pitts, Alpha-structural recursion and induction, Journal of the ACM, vol.53, issue.3, pp.459-506, 2006.
DOI : 10.1145/1147954.1147961
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.518

G. Plotkin, A Structural Approach to Operational Semantics, Journal of Logic and Algebraic Programming, pp.60-6117, 2004.

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 S. Berghofer, A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL, Proc. of the 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of LNAI, pp.498-512, 2006.
DOI : 10.1007/11814771_41

C. Urban, J. Cheney, and S. Berghofer, Mechanizing the Metatheory of LF, Proc. of the 23rd IEEE Symposium on Logic in Computer Science (LICS), pp.45-56, 2008.

C. Urban and C. Tasson, Nominal Techniques in Isabelle/HOL, Proc. of the 20th International Conference on Automated Deduction (CADE), pp.38-53, 2005.

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, Proc. of the 12th Conference on Theorem Proving in Higher Order Logics (TPHOLs), number 1690 in LNCS, pp.167-184, 1999.
DOI : 10.1007/3-540-48256-3_12