Show simple item record

dc.contributor.authorMalecha, Gregory Michael
dc.contributor.authorChlipala, Adam
dc.contributor.authorBaibant, Thomas
dc.date.accessioned2014-07-21T13:59:59Z
dc.date.issued2014
dc.identifierQuick submit: 2014-06-06T08:42:22-04:00
dc.identifier.citationMalecha, Gregory, Adam Chlipala, and Thomas Braibant. 2014. “Compositional Computational Reflection.” Lecture Notes in Computer Science: 374–389.en_US
dc.identifier.isbn978-3-319-08969-0en_US
dc.identifier.isbn978-3-319-08970-6en_US
dc.identifier.issn0302-9743en_US
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:12537617
dc.description.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.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dc.publisherSpringer Science + Business Mediaen_US
dc.relation.isversionofdoi:10.1007/978-3-319-08970-6_24en_US
dc.relation.hasversionhttp://adam.chlipala.net/papers/MirrorShardITP14/MirrorShardITP14.pdfen_US
dc.relation.hasversionhttp://www.people.fas.harvard.edu/~gmalecha/pub/ccr-itp14.pdfen_US
dash.licenseLAA
dc.subjectComputational reflectionen_US
dc.subjectautomationen_US
dc.subjectCoqen_US
dc.subjectverificationen_US
dc.titleCompositional Computational Reflectionen_US
dc.typeJournal Articleen_US
dc.date.updated2014-06-06T12:42:22Z
dc.description.versionAccepted Manuscripten_US
dc.rights.holderGregory Malecha, Adam Chlipala, Thomas Baibant
dc.relation.journalLecture Notes in Computer Scienceen_US
dash.depositing.authorMalecha, Gregory Michael
dc.date.available2014-07-21T13:59:59Z
dc.relation.bookInteractive Theorem Provingen_US
dc.identifier.doi10.1007/978-3-319-08970-6_24*
workflow.legacycommentsFLAG3 Malecha - author emailed on 7/9/2014en_US
dash.authorsorderedfalse
dash.contributor.affiliatedMalecha, Gregory Michael
dc.identifier.orcid0000-0003-3952-0807


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record