Compositional Computational Reflection

DSpace/Manakin Repository

Compositional Computational Reflection

Citable link to this page


Title: Compositional Computational Reflection
Author: Malecha, Gregory Michael; Chlipala, Adam; Baibant, Thomas

Note: Order does not necessarily reflect citation order of authors.

Citation: Malecha, Gregory, Adam Chlipala, and Thomas Braibant. 2014. “Compositional Computational Reflection.” Lecture Notes in Computer Science: 374–389.
Full Text & Related Files:
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.
Published Version: doi:10.1007/978-3-319-08970-6_24
Other Sources:
Terms of Use: This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at
Citable link to this page:
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search