Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac
Author(s)
Gross, Jason; Erbsen, Andres; Chlipala, Adam
DownloadAccepted version (1.322Mb)
Alternative title
Fast Setup for Proof by Reflection, in Two Lines of Ltac
Terms of use
Metadata
Show full item recordAbstract
© 2018, Springer International Publishing AG, part of Springer Nature. 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 compilers or procedures in the proof-by-reflection style. Our new strategy, based on simple generalization of subterms as variables, is straightforward, short, and fast. In its pure form, it is only complete for constants and function applications, but “let” binders, eliminators, lambdas, and quantifiers can be accommodated through lightweight coding conventions or preprocessing. We survey the existing methods of reification across multiple Coq metaprogramming facilities, describing various design choices and tricks that can be used to speed them up, as well as various limitations. We report benchmarking results for 18 variants, 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; writing an OCaml plugin is the only method tested to be faster. Our method is the most concise of the strategies we considered, reifying terms using only two to four lines of Ltac—beyond lists of the identifiers to reify and their reified variants. Additionally, our strategy automatically provides error messages that are no less helpful than Coq’s own error messages.
Date issued
2018Department
Massachusetts Institute of Technology. Computer Science and Artificial Intelligence LaboratoryPublisher
Springer International Publishing
Citation
Gross, Jason, Erbsen, Andres and Chlipala, Adam. 2018. "Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac."
Version: Author's final manuscript
ISSN
0302-9743
1611-3349