A Formalization of the Strong Normalisation Proof for System F in LEGO, Proc. of TLCA, pp.13-28, 1993. ,
Engineering Aspects of Formal Metatheory, 2007. ,
Logical Relations and a Case Study in Equivalence Checking, Advanced Topics in Types and Programming Languages, pp.223-244, 2005. ,
Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, 2007. ,
DOI : 10.1006/inco.2001.2951
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
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
Towards a Judgemental Reconstruction of Logical Relation Proofs, 2007. ,
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
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
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
Nominal Techniques in Isabelle/HOL, Proc. of the 20th International Conference on Automated Deduction (CADE), pp.38-53, 2005. ,
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