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: http://adam.chlipala.net/papers/MirrorShardITP14/MirrorShardITP14.pdf
http://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#LAA
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:12537617

Show full Dublin Core record

This item appears in the following Collection(s)

  • FAS Scholarly Articles [7219]
    Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University
 
 

Search DASH


Advanced Search
 
 

Submitters