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?
It's time for you to meet Edwin Brady:

http://edwinb.wordpress.com/publications/

His earliest papers are about designing DSLs to solve very concrete problems. Lately, he has also been working on optimizing their performance (using type theoretic tools!).

To explore this design space, I would recommend playing with Agda or Idris.