Reification of Shallow-Embedded DSLs in Coq with Automated Verification
Shallow and deep embeddings of DSLs have their pros and cons. For example, shallow embedding is excellent for quick prototyping, as it allows quick extension or modification of the embedded language. Meanwhile, deep embedding is better suited for code transformation and compilation. Thus, it might be useful to be able to switch from shallow to deep embedding while making sure the semantics of the embedded language are preserved. We will demonstrate a working approach for implementing and proving such conversion using TemplateCoq.
Sat 19 JanDisplayed time zone: Belfast change
14:00 - 15:30
|Reification of Shallow-Embedded DSLs in Coq with Automated Verification
|Reifying and Translating a Monadic Fragment of Gallina
|Session with the Coq Development Team