Show simple item record

dc.contributor.authorMalecha, Gregory Michael
dc.contributor.authorMorrisett, Greg Gregory
dc.contributor.authorShinnar, Avraham
dc.contributor.authorWisnesky, Ryan
dc.date.accessioned2013-11-14T12:54:13Z
dc.date.issued2010
dc.identifier.citationMalecha, Gregory, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. 2010. “Toward a verified relational database management system.” In Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL 10, 237. Association for Computing Machinery. doi:10.1145/1706299.1706329. http://dx.doi.org/10.1145/1706299.1706329.en_US
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:11318529
dc.description.abstractWe report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations that are proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for (finite) relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dc.publisherAssociation for Computing Machineryen_US
dc.relation.isversionofdoi:10.1145/1706299.1706329en_US
dc.relation.hasversionhttp://www.eecs.harvard.edu/~ryan/en_US
dash.licenseLAA
dc.titleToward a verified relational database management systemen_US
dc.typeConference Paperen_US
dc.description.versionAccepted Manuscripten_US
dc.relation.journalProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10en_US
dash.depositing.authorMorrisett, Greg Gregory
dash.waiver2009-12-08
dc.date.available2013-11-14T12:54:13Z
dc.identifier.doi10.1145/1706299.1706329*
workflow.legacycommentsReasoning that we can post the manuscript because of the ACM's default policies. http://www.sherpa.ac.uk/romeo/pub/21/en_US
dash.contributor.affiliatedShinnar, Avraham Ever
dash.contributor.affiliatedWisnesky, Ryan
dash.contributor.affiliatedMalecha, Gregory Michael
dash.contributor.affiliatedMorrisett, Greg Gregory
dc.identifier.orcid0000-0003-3952-0807


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record