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.