Compositional Computational Reflection
View/ Open
Author
Chlipala, Adam
Baibant, Thomas
Note: Order does not necessarily reflect citation order of authors.
Published Version
https://doi.org/10.1007/978-3-319-08970-6_24Metadata
Show full item recordCitation
Malecha, Gregory, Adam Chlipala, and Thomas Braibant. 2014. “Compositional Computational Reflection.” Lecture Notes in Computer Science: 374–389.Abstract
Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof- generating tactic language such as Ltac. This composition, however, comes at the cost of both larger proof terms and redundant preprocessing. In this work, we propose a methodology for writing composable reflective procedures that solve many small tasks in a single invocation. The key technical insights are techniques for reasoning semantically about extensible syntax in intensional type theory. Our techniques make it possible to compose sound procedures and write generic procedures parametrized by lemmas mimicking Coq’s support for hint databases.Other Sources
http://adam.chlipala.net/papers/MirrorShardITP14/MirrorShardITP14.pdfhttp://www.people.fas.harvard.edu/~gmalecha/pub/ccr-itp14.pdf
Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAACitable link to this page
http://nrs.harvard.edu/urn-3:HUL.InstRepos:12537617
Collections
- FAS Scholarly Articles [18292]
Contact administrator regarding this item (to report mistakes or request changes)