  We describe a new approach to domain specific languages (DSLs), called Quoted
DSLs (QDSLs), that resurrects two old ideas: quotation, from McCarthy's Lisp of
1960, and the subformula property, from Gentzen's natural deduction of 1935.
Quoted terms allow the DSL to share the syntax and type system of the host
language. Normalising quoted terms ensures the subformula property, which
guarantees that one can use higher-order types in the source while guaranteeing
first-order types in the target, and enables using types to guide fusion. We
test our ideas by re-implementing Feldspar, which was originally implemented as
an Embedded DSL (EDSL), as a QDSL; and we compare the QDSL and EDSL variants.
