<p>It's time for you to meet Edwin Brady:</p>

<p><a href="http://edwinb.wordpress.com/publications/">http://edwinb.wordpress.com/publications/</a></p>

<p>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!).</p>

<p>To explore this design space, I would recommend playing with Agda or Idris. </p>

CC BY-SA 3.0
2013-03-25T10:51:57.733Z
2013-03-25T10:51:57.733Z
pedagand
<p>Edwin Brady's work is very relevant. Also relevant:</p>

<ul>
<li>Neil Sculthorpe and Henrik Nilsson used dependent types for FRP, e.g., <a href="http://www.cs.nott.ac.uk/~nhn/Publications/hosc2011.pdf" rel="nofollow"><em>Keeping Calm in the Face of Change: Towards Optimization of FRP by Reasoning About Change</em></a></li>
<li>So did Alan Jeffrey: <a href="http://ect.bell-labs.com/who/ajeffrey/papers/padl13.pdf" rel="nofollow"><em>Dependently Typed Web Client Applications: FRP in Agda in HTML5</em></a></li>
<li>Zachary Tetlock and Sorin Lerner wrote a paper about extending the Compcert verified compiler with a DSL for writing provably correct code transformations: <a href="http://cseweb.ucsd.edu/~lerner/papers/pldi10-xcert.html" rel="nofollow"><em>Bringing Extensibility to Verified Compilers</em></a></li>
</ul>

CC BY-SA 3.0
2013-03-25T11:39:10.670Z
2013-03-25T11:39:10.670Z
Neel Krishnaswami
<p>(this is a beginner question and English is not my first language)</p>

<p>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).</p>

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

<p>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.</p>

<p>I found only two references:</p>

<p>Oury, Nicolas, and Wouter Swierstra. <a href="http://dl.acm.org/citation.cfm?id=1411213" rel="nofollow">"The power of Pi."</a> ACM Sigplan Notices. Vol. 43. No. 9. ACM, 2008.</p>

<p>Chlipala, Adam. "<a href="http://adam.chlipala.net/papers/UrPLDI10/" rel="nofollow">Ur: statically-typed metaprogramming with type-level record computation."</a> ACM Sigplan Notices. Vol. 45. No. 6. ACM, 2010.</p>

<p>Any suggestions on papers that I missed? </p>

<reference-request><dependent-type>
dependent types and higher-order logic applied in the realm of DSLs
mrsteve
# dependent types and higher-order logic applied in the realm of DSLs

(Asked by: username_0 on 2013-03-25)

(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."](http://dl.acm.org/citation.cfm?id=1411213) ACM Sigplan Notices. Vol. 43. No. 9. ACM, 2008.

Chlipala, Adam. "[Ur: statically-typed metaprogramming with type-level record computation."](http://adam.chlipala.net/papers/UrPLDI10/) ACM Sigplan Notices. Vol. 45. No. 6. ACM, 2010.

Any suggestions on papers that I missed?

**Tags:** reference-request, dependent-type

---

## 2 answers

### Answer by username_1 on 2013-03-25. Score: 6

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.


---

### Answer by username_2 on 2013-03-25. Score: 4

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

* Neil Sculthorpe and Henrik Nilsson used dependent types for FRP, e.g., [*Keeping Calm in the Face of Change: Towards Optimization of FRP by Reasoning About Change*](http://www.cs.nott.ac.uk/~nhn/Publications/hosc2011.pdf)
* So did Alan Jeffrey: [*Dependently Typed Web Client Applications: FRP in Agda in HTML5*](http://ect.bell-labs.com/who/ajeffrey/papers/padl13.pdf)
* Zachary Tetlock and Sorin Lerner wrote a paper about extending the Compcert verified compiler with a DSL for writing provably correct code transformations: [*Bringing Extensibility to Verified Compilers*](http://cseweb.ucsd.edu/~lerner/papers/pldi10-xcert.html)


---

