Writing plugins and proving them correct in MetaCoq

Bohdan Liesnikov

Date: Wed, June 03, 2020
Time: 13:00
Room: Eelco's Zoom Room

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 |