Writing plugins and proving them correct in MetaCoq

Bohdan Liesnikov

Writing and extending plugins for Coq in OCaml without extensive familiarity with Coq internals is a challenging task. Fortunately, MetaCoq not only facilitates such tasks, but also provides means for proving correctness of the written plugins. I worked on a plugin that implements subterm relations from the Equations package for Coq. It turned out that while writing the plugin is indeed made simpler by the MetaCoq machinery, there’s still room for improvement in the realm of proofs. I’m also going to talk about other examples of plugins that have been written in MetaCoq and how my experience compares to those cases.

---

Previous: Jonas Kastberg Hinrichsen | Machine-Checked Semantic Session Typing
Next: Jesper Cockx | Revising Agda's module system