Charla: "MetaCoq: Tactics for Coq, in Coq”

Beta Ziliani, U de Córdoba
22 Mayo, 2017 - 11:00
Auditorio Ramón Picarte
Prof. Éric Tanter


During my PhD I developed Mtac. This language covers essentially the fragment of Ltac that allows for meta-programming in Coq; the "constr" fragment. But, unlike Ltac's constr, Mtac is typed, and have reasonable semantics. In certain proof development, like when doing "proof by reflection", Mtac is a great tool for Coq users to have at hand [1]. However, most Coq users rarely find themselves the need to work with this restricted fragment of Ltac, and therefore will see no gain in adopting Mtac.


MetaCoq is an extension to Mtac intended as an (almost) full replacement for Ltac, allowing for the development of typed tactics. This talk introduces MetaCoq and its coming developments.