Compositional Computational Reflection

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. We also consider how users can customize the behavior of reflective procedures by packaging additional information and passing it to them. This mimicks Coq's usual support for hint databases with only slightly more user effort. We evaluate our techniques in the context of imperative program verification.