Here is a tar-gzipped directory containing the theory files for the paper Theory Support for Weak Higher Order Abstract Syntax in Isabelle/HOL.

Here is a tar-gzipped directory containing the theory files for the papers Strong normalization for System F by HOAS on top of FOAS and Recursion principles for syntax with bindings and substitution.