Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac
© 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 pro...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Springer International Publishing
2021
|
| Online Access: | https://hdl.handle.net/1721.1/137403 |
| _version_ | 1811072344202936320 |
|---|---|
| author | Gross, Jason Erbsen, Andres Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Gross, Jason Erbsen, Andres Chlipala, Adam |
| author_sort | Gross, Jason |
| collection | MIT |
| description | © 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. |
| first_indexed | 2024-09-23T09:04:30Z |
| format | Article |
| id | mit-1721.1/137403 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T09:04:30Z |
| publishDate | 2021 |
| publisher | Springer International Publishing |
| record_format | dspace |
| spelling | mit-1721.1/1374032022-09-30T13:15:22Z Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac Fast Setup for Proof by Reflection, in Two Lines of Ltac Gross, Jason Erbsen, Andres Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory © 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. 2021-11-04T19:19:42Z 2021-11-04T19:19:42Z 2018 2019-05-13T17:56:37Z Article http://purl.org/eprint/type/JournalArticle 0302-9743 1611-3349 https://hdl.handle.net/1721.1/137403 Gross, Jason, Erbsen, Andres and Chlipala, Adam. 2018. "Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac." en 10.1007/978-3-319-94821-8_17 Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer International Publishing MIT web domain |
| spellingShingle | Gross, Jason Erbsen, Andres Chlipala, Adam Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title | Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title_full | Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title_fullStr | Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title_full_unstemmed | Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title_short | Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac |
| title_sort | reification by parametricity fast setup for proof by reflection in two lines of ltac |
| url | https://hdl.handle.net/1721.1/137403 |
| work_keys_str_mv | AT grossjason reificationbyparametricityfastsetupforproofbyreflectionintwolinesofltac AT erbsenandres reificationbyparametricityfastsetupforproofbyreflectionintwolinesofltac AT chlipalaadam reificationbyparametricityfastsetupforproofbyreflectionintwolinesofltac AT grossjason fastsetupforproofbyreflectionintwolinesofltac AT erbsenandres fastsetupforproofbyreflectionintwolinesofltac AT chlipalaadam fastsetupforproofbyreflectionintwolinesofltac |