Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 14:00 - 14:25 at Sala VI - Contributed Talks 3 & Coq Developers Chair(s): Qinxiang Cao

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.

Slides (vzaliva-CoqPL19-slides.pdf)236KiB
Abstract (coqpl19-final2.pdf)448KiB

Sat 19 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Contributed Talks 3 & Coq DevelopersCoqPL at Sala VI
Chair(s): Qinxiang Cao Shanghai Jiao Tong University
14:00
25m
Talk
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
CoqPL
Vadim Zaliva Carnegie Mellon University, USA, Matthieu Sozeau Inria
File Attached
14:25
25m
Talk
Reifying and Translating a Monadic Fragment of Gallina
CoqPL
File Attached
14:50
40m
Demonstration
Session with the Coq Development Team
CoqPL