4
$\begingroup$

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

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

Edwin Brady's work is very relevant. Also relevant:

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.