(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?