T. Altenkirch, A Formalization of the Strong Normalisation Proof for System F in LEGO, Proc. of TLCA, pp.13-28, 1993.

B. Aydemir, A. Charguéraud, B. C. Pierce, and S. Weirich, Engineering Aspects of Formal Metatheory, 2007.

K. Crary, Logical Relations and a Case Study in Equivalence Checking, Advanced Topics in Types and Programming Languages, pp.223-244, 2005.

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

J. Mckinna and R. Pollack, Pure type systems formalized, Proc. of the International Conference on Typed Lambda Calculi and Applications (TLCA), number 664 in LNCS, pp.289-305, 1993.
DOI : 10.1007/BFb0037113

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

C. Schürmann and J. Sarnat, Towards a Judgemental Reconstruction of Logical Relation Proofs, 2007.

W. W. Tait, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, pp.198-212, 1967.
DOI : 10.1007/BF01447860

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, S. Berghofer, and M. Norrish, Barendregt???s Variable Convention in Rule Inductions, Proc. of the 21th International Conference on Automated Deduction (CADE), 2007.
DOI : 10.1007/978-3-540-73595-3_4

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 International 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