Nominal logical frameworks

Is there a sensible way of combining nominal logic ideas with
established logical frameworks such as LF or the Calculus of
Constructions, that reconciles constructive and propositions-
(judgments)-as-types, proofs-as-programs techniques with abstract
syntax?

Is there a principled way of combining the advantages of
higher-order abstract syntax (namely, built-in capture-avoiding
substitution) with nominal syntax?  Is there a principled way to
integrate (and generalize) LF's higher-order judgment methodology
(wherein the LF context is used to store local parameters and local
hypotheses of the object language) with nominal or other more
foundational techniques?

James Cheney