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. We also consider sound methods for user extension of such procedures using lemmas and full reflective procedures, which mimicks Coq's support for hint databases with only slightly more user effort.
Source code is available for the framework and the instantiation for Bedrock