Compositional Computational Reflection
Baibant, ThomasNote: Order does not necessarily reflect citation order of authors.
MetadataShow full item record
CitationMalecha, Gregory, Adam Chlipala, and Thomas Braibant. 2014. “Compositional Computational Reflection.” Lecture Notes in Computer Science: 374–389.
AbstractCurrent 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.
Citable link to this pagehttp://nrs.harvard.edu/urn-3:HUL.InstRepos:12537617
- FAS Scholarly Articles