Copyrights to these papers may be held by the publishers. The download files are preprints. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Vadim Zaliva and Matthieu Sozeau (Proc. International Workshop on Coq for Programming Languages (CoqPL), 2019)
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
Bibtex