Reification by Parametricity

Authors: Jason Gross, Andres Erbsen and Adam Chlipala

Paper Information

Title:Reification by Parametricity
Authors:Jason Gross, Andres Erbsen and Adam Chlipala
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:Coq, reification, proof assistants, proof engineering, proof by reflection

ABSTRACT. We present a new strategy for performing reification in Coq. That is, we show how to generate first-class abstract syntax trees from ``native'' terms of Coq's logic, suitable as inputs to verified proof procedures in the *proof by reflection* style. Our new strategy, based on the pattern tactic, is simple, short, and fast. We survey the existing methods of reification, describing various design choices and tricks that can be used to speed them up, as well as various limitations. Our strategy is not a good fit, for example, when a term must be reified without performing βιζ reduction. We describe the results of benchmarking 18 variants of reification, in addition to our own, finding that our own reification outperforms 16 of these methods in all cases, and one additional method in some cases; the fastest method of reification we tested is writing an OCaml plugin. Our method is the most concise of the strategies we considered, requiring only two to four lines of Ltac---beyond lists of the identifiers to reify and their reified variants---to reify a term. Additionally, our strategy automatically provides error messages which are no less helpful than Coq's own error messages.

Talk:Jul 10 14:30 (Session 55C)