dependent types and higher-order logic applied in the realm of DSLs

(this is a beginner question and English is not my first language)

I am searching for references on using theorem proves based on dependent type theory (or Martin Löf type-theory) and higher-order logic in the development of domain specific languages (DSLs).

Dependent types, i.e., Coq and Agda Higher-Order logic, i.e., Isabelle/HOL

Currently, I am attending an course on higher-order logic for PhD students, and it seems to me there are possible applications to DSLs. As I am not so familiar with Coq so I may have overlooked some references.

I found only two references:

Oury, Nicolas, and Wouter Swierstra. "The power of Pi." ACM Sigplan Notices. Vol. 43. No. 9. ACM, 2008.

Chlipala, Adam. "Ur: statically-typed metaprogramming with type-level record computation." ACM Sigplan Notices. Vol. 45. No. 6. ACM, 2010.

Any suggestions on papers that I missed?